source: src/ASM/AssemblyProof.ma @ 1484

Last change on this file since 1484 was 1484, checked in by sacerdot, 8 years ago

...

File size: 88.7 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4
5definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
6  λP.
7    P true ∧ P false.
8 
9let rec bitvector_elim_prop_internal
10  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
11  match m return λm. m ≤ n → BitVector (n - m) → Prop with
12  [ O    ⇒ λprf1. λprefix. P ?
13  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
14  ].
15  [ applyS prefix
16  | letin res ≝ (bit ::: prefix)
17    < (minus_S_S ? ?)
18    > (minus_Sn_m ? ?)
19  [ @ res
20  | @ prf2
21  ]
22  | /2/
23  ].
24qed.
25
26definition bitvector_elim_prop ≝
27  λn: nat.
28  λP: BitVector n → Prop.
29    bitvector_elim_prop_internal n P n ? ?.
30  [ @ (le_n ?)
31  | < (minus_n_n ?)
32    @ [[ ]]
33  ]
34qed.
35
36lemma bool_eq_internal_eq:
37  ∀b, c.
38    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
39  #b #c
40  cases b
41  [ normalize //
42  | normalize
43    cases c
44    [ normalize //
45    | normalize //
46    ]
47  ]
48qed.
49
50definition bit_elim: ∀P: bool → bool. bool ≝
51  λP.
52    P true ∧ P false.
53
54let rec bitvector_elim_internal
55  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
56  match m return λm. m ≤ n → BitVector (n - m) → bool with
57  [ O    ⇒ λprf1. λprefix. P ?
58  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
59  ].
60  [ applyS prefix
61  | letin res ≝ (bit ::: prefix)
62    < (minus_S_S ? ?)
63    > (minus_Sn_m ? ?)
64    [ @ res
65    | @ prf2
66    ]
67  | /2/
68  ].
69qed.
70
71definition bitvector_elim ≝
72  λn: nat.
73  λP: BitVector n → bool.
74    bitvector_elim_internal n P n ? ?.
75  [ @ (le_n ?)
76  | < (minus_n_n ?)
77    @ [[ ]]
78  ]
79qed.
80
81lemma super_rewrite2:
82 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
83  ∀P: ∀m. Vector A m → Prop.
84   n=m → v1 ≃ v2 → P n v1 → P m v2.
85 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
86qed.
87
88lemma vector_cons_append:
89  ∀A: Type[0].
90  ∀n: nat.
91  ∀e: A.
92  ∀v: Vector A n.
93    e ::: v = [[ e ]] @@ v.
94  # A # N # E # V
95  elim V
96  [ normalize %
97  | # NN # AA # VV # IH
98    normalize
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 | % ]
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
1070lemma split_zero:
1071  ∀A,m.
1072  ∀v: Vector A m.
1073    〈[[]], v〉 = split A 0 m v.
1074  #A #m #v
1075  elim v
1076  [ %
1077  | #n #hd #tl #ih
1078    normalize in ⊢ (???%) %
1079  ]
1080qed.
1081
1082lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
1083 #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
1084 #n #hd #tl #abs @⊥ destruct (abs)
1085qed.
1086
1087lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
1088 ∃hd.∃tl.v ≃ VCons A n hd tl.
1089 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
1090 [ #abs @⊥ destruct (abs)
1091 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
1092qed.
1093
1094lemma vector_append_zero:
1095  ∀A,m.
1096  ∀v: Vector A m.
1097  ∀q: Vector A 0.
1098    v = q@@v.
1099  #A #m #v #q
1100  >(Vector_O A q) %
1101qed.
1102
1103lemma prod_eq_left:
1104  ∀A: Type[0].
1105  ∀p, q, r: A.
1106    p = q → 〈p, r〉 = 〈q, r〉.
1107  #A #p #q #r #hyp
1108  >hyp %
1109qed.
1110
1111lemma prod_eq_right:
1112  ∀A: Type[0].
1113  ∀p, q, r: A.
1114    p = q → 〈r, p〉 = 〈r, q〉.
1115  #A #p #q #r #hyp
1116  >hyp %
1117qed.
1118
1119corollary prod_vector_zero_eq_left:
1120  ∀A, n.
1121  ∀q: Vector A O.
1122  ∀r: Vector A n.
1123    〈q, r〉 = 〈[[ ]], r〉.
1124  #A #n #q #r
1125  generalize in match (Vector_O A q …)
1126  #hyp
1127  >hyp in ⊢ (??%?)
1128  %
1129qed.
1130
1131axiom split_succ:
1132  ∀A, m, n.
1133  ∀l: Vector A m.
1134  ∀r: Vector A n.
1135  ∀v: Vector A (m + n).
1136  ∀hd: A.
1137    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
1138(*
1139  #A #m
1140  elim m
1141  [ #n #l #r #v #hd #equal #hyp
1142    normalize >(Vector_O A l) >equal
1143    >(Vector_O A l) %
1144  | #n' #ih #n #l #r #v #hd
1145    #equal #hyp
1146    cases(Vector_Sn A n' l)
1147    #hd' #exists
1148    cases exists #tl #jmeq
1149    >jmeq *)
1150
1151lemma split_prod:
1152  ∀A,m,n.
1153  ∀p: Vector A (m + n).
1154  ∀v: Vector A m.
1155  ∀q: Vector A n.
1156    p = v@@q → 〈v, q〉 = split A m n p.
1157  #A #m
1158  elim m
1159  [ #n #p #v #q #hyp
1160    >hyp <(vector_append_zero A n q v)
1161    >(prod_vector_zero_eq_left A …)
1162    @split_zero
1163  | #r #ih #n #p #v #q #hyp
1164    >hyp
1165    cases (Vector_Sn A r v)
1166    #hd #exists
1167    cases exists
1168    #tl #jmeq >jmeq
1169    @split_succ [1: % |2: @ih % ]
1170  ]
1171qed.
1172
1173(*
1174lemma split_prod_exists:
1175  ∀A, m, n.
1176  ∀p: Vector A (m + n).
1177  ∃v: Vector A m.
1178  ∃q: Vector A n.
1179    〈v, q〉 = split A m n p.
1180  #A #m #n #p
1181  elim m
1182  @ex_intro
1183  [1:
1184  |2: @ex_intro
1185      [1:
1186      |2:
1187      ]
1188  ]
1189*)
1190
1191axiom split_elim:
1192 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
1193  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
1194(*  #A #l #m #v #P #hyp
1195  normalize
1196  <(split_prod A l m v ? ? ?)
1197*)
1198
1199example half_add_SO:
1200 ∀pc.
1201 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
1202 cases daemon.
1203qed.
1204
1205(*
1206axiom not_eqvb_S:
1207 ∀pc.
1208 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
1209
1210axiom not_eqvb_SS:
1211 ∀pc.
1212 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
1213 
1214axiom bitvector_elim_complete:
1215 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
1216
1217lemma bitvector_elim_complete':
1218 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
1219 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
1220 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
1221qed.
1222*)
1223
1224(*
1225lemma andb_elim':
1226 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
1227 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
1228qed.
1229*)
1230
1231let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
1232                       (encoding: list Byte) on encoding: Prop ≝
1233  match encoding with
1234  [ nil ⇒ final_pc = pc
1235  | cons hd tl ⇒
1236    let 〈new_pc, byte〉 ≝ next code_memory pc in
1237      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
1238  ].
1239
1240lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
1241 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
1242  let intermediate_pc ≝ pc + length … l1 in
1243   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
1244    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
1245 #code_memory #final_pc #l1 elim l1
1246  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
1247  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
1248    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
1249qed.
1250
1251axiom bitvector_3_elim_prop:
1252 ∀P: BitVector 3 → Prop.
1253  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
1254  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
1255  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
1256
1257definition ticks_of_instruction ≝
1258 λi.
1259  let trivial_code_memory ≝ assembly1 i in
1260  let trivial_status ≝ load_code_memory trivial_code_memory in
1261   \snd (fetch trivial_status (zero ?)).
1262
1263lemma fetch_assembly:
1264  ∀pc,i,code_memory,assembled.
1265    assembled = assembly1 i →
1266      let len ≝ length … assembled in
1267      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1268      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
1269      let 〈instr_pc, ticks〉 ≝ fetched in
1270      let 〈instr,pc'〉 ≝ instr_pc in
1271       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
1272 #pc #i #code_memory #assembled cases i [8: *]
1273 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
1274 [47,48,49:
1275 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
1276  [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,
1277   59,60,63,64,65,66,67: #ARG]]
1278 [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,
1279  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
1280  [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,
1281   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,
1282   68,69,70,71: #ARG2]]
1283 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
1284 normalize in ⊢ (???% → ?)
1285 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
1286  normalize in ⊢ (???% → ?)]
1287 #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
1288 try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
1289 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
1290 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
1291 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
1292 [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,
1293  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,
1294  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
1295 whd >eq_instruction_refl >H4 @eq_bv_refl
1296qed.
1297
1298let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
1299 match expected with
1300  [ nil ⇒ eq_bv … pc final_pc = true
1301  | cons i tl ⇒
1302     let fetched ≝ fetch code_memory pc in
1303     let 〈instr_pc, ticks〉 ≝ fetched in
1304     let 〈instr,pc'〉 ≝ instr_pc in
1305      eq_instruction instr i = true ∧
1306      ticks = (ticks_of_instruction i) ∧
1307      fetch_many code_memory final_pc pc' tl].
1308
1309lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1310 #A #a #b #EQ destruct //
1311qed.
1312
1313axiom eq_instruction_to_eq:
1314  ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
1315               
1316
1317notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
1318interpretation "dp" 'dp x y = (dp x y).
1319
1320lemma fetch_assembly_pseudo':
1321 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
1322  ∀pi,code_memory,len,assembled,instructions,pc.
1323   let expansion ≝ pol ppc in
1324   Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
1325    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction_safe program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
1326     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1327      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
1328 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
1329 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
1330 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
1331 >EQ2a >EQ2b -EQ2a EQ2b;
1332  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
1333  generalize in match pc elim instructions
1334  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
1335  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
1336    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
1337    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
1338    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
1339    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
1340    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
1341qed.
1342
1343axiom bitvector_of_nat_nat_of_bitvector:
1344  ∀n,v.
1345    bitvector_of_nat n (nat_of_bitvector n v) = v.
1346
1347(* CSC: soo long next one; can we merge with previous one now? *)
1348lemma fetch_assembly_pseudo:
1349 ∀program.∀pol:policy program.∀ppc.
1350  ∀code_memory.
1351   let lookup_labels ≝ ? in
1352   let lookup_datalabels ≝ ? in
1353   let pc ≝ ? in
1354   let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
1355   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in
1356   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
1357     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
1358      fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
1359 #program #pol #ppc #code_memory
1360 letin lookup_labels ≝ (λx:Identifier
1361    .sigma program pol (address_of_word_labels_code_mem (\snd  program) x))
1362 letin lookup_datalabels ≝
1363  (λx:BitVector 16
1364    .lookup Identifier 16 x (construct_datalabels (\fst  program)) (zero 16))
1365 letin pc ≝ (sigma program pol ppc)
1366 letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
1367 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …))
1368 @pair_elim' #len #assembled #EQ1 #H
1369 generalize in match
1370  (fetch_assembly_pseudo' program pol ppc lookup_labels lookup_datalabels pi
1371  code_memory len assembled instructions (nat_of_bitvector ? pc) ???) in ⊢ ?;
1372 [ >bitvector_of_nat_nat_of_bitvector //
1373 | >bitvector_of_nat_nat_of_bitvector normalize nodelta >(sig2 ?? (expand_pseudo_instruction …)) %
1374 | >bitvector_of_nat_nat_of_bitvector <EQ1 @assembly_1_pseudoinstruction_ok1
1375 | //]
1376qed.
1377
1378(* This is a trivial consequence of fetch_assembly + the proof that the
1379   function that load the code in memory is correct. The latter is based
1380   on missing properties from the standard library on the BitVectorTrie
1381   data structrure. *)
1382axiom assembly_ok:
1383 ∀program,pol,assembled,costs'.
1384  let 〈labels,costs〉 ≝ build_maps program pol in
1385  〈assembled,costs'〉 = assembly program pol →
1386  costs = costs' ∧
1387  let code_memory ≝ load_code_memory assembled in
1388  let preamble ≝ \fst program in
1389  let datalabels ≝ construct_datalabels preamble in
1390  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1391  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1392  ∀ppc.
1393  let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
1394   ∀len,assembledi.
1395     〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) →
1396      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
1397       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
1398
1399lemma fetch_assembly_pseudo2:
1400 ∀program,pol,ppc.
1401(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
1402  let assembled ≝ \fst (assembly program pol) in
1403  let code_memory ≝ load_code_memory assembled in
1404  let data_labels ≝ construct_datalabels (\fst program) in
1405  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1406  let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1407  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1408  let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
1409   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
1410 * #preamble #instr_list #pol #ppc
1411 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
1412 letin code_memory ≝ (load_code_memory assembled)
1413 letin data_labels ≝ (construct_datalabels preamble)
1414 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
1415 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1416 @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
1417 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
1418 @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
1419 #H cases (H (refl \ldots)) -H; #EQ3
1420 generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
1421 cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
1422 #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
1423 generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
1424 >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
1425 >H2 #K @K
1426qed.
1427
1428(* OLD?
1429definition assembly_specification:
1430  ∀assembly_program: pseudo_assembly_program.
1431  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1432  λpseudo_assembly_program.
1433  λcode_mem.
1434    ∀pc: Word.
1435      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1436      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1437      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1438      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1439      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1440       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1441      match pre_assembled with
1442       [ None ⇒ True
1443       | Some pc_code ⇒
1444          let 〈new_pc,code〉 ≝ pc_code in
1445           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1446
1447axiom assembly_meets_specification:
1448  ∀pseudo_assembly_program.
1449    match assembly pseudo_assembly_program with
1450    [ None ⇒ True
1451    | Some code_mem_cost ⇒
1452      let 〈code_mem, cost〉 ≝ code_mem_cost in
1453        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1454    ].
1455(*
1456  # PROGRAM
1457  [ cases PROGRAM
1458    # PREAMBLE
1459    # INSTR_LIST
1460    elim INSTR_LIST
1461    [ whd
1462      whd in ⊢ (∀_. %)
1463      # PC
1464      whd
1465    | # INSTR
1466      # INSTR_LIST_TL
1467      # H
1468      whd
1469      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1470    ]
1471  | cases not_implemented
1472  ] *)
1473*)
1474
1475definition internal_pseudo_address_map ≝ list (BitVector 8).
1476
1477axiom low_internal_ram_of_pseudo_low_internal_ram:
1478 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1479
1480axiom high_internal_ram_of_pseudo_high_internal_ram:
1481 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1482
1483axiom low_internal_ram_of_pseudo_internal_ram_hit:
1484 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
1485  member ? (eq_bv 8) (false:::addr) M = true →
1486   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1487   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1488   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1489   let bl ≝ lookup ? 7 addr ram (zero 8) in
1490   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1491    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
1492
1493(* changed from add to sub *)
1494axiom low_internal_ram_of_pseudo_internal_ram_miss:
1495 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
1496  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1497  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1498  let carr ≝ get_index_v ? ? flags 1 ? in
1499  carr = false →
1500  member ? (eq_bv 8) (false:::Saddr) M = false →
1501   member ? (eq_bv 8) (false:::addr) M = false →
1502    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1503  //
1504qed.
1505
1506definition addressing_mode_ok ≝
1507 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
1508  λaddr:addressing_mode.
1509   match addr with
1510    [ DIRECT d ⇒
1511       ¬(member ? (eq_bv 8) d M) ∧
1512       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1513    | INDIRECT i ⇒
1514       let d ≝ get_register ? s [[false;false;i]] in
1515       ¬(member ? (eq_bv 8) d M) ∧
1516       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1517    | EXT_INDIRECT _ ⇒ true
1518    | REGISTER _ ⇒ true
1519    | ACC_A ⇒ true
1520    | ACC_B ⇒ true
1521    | DPTR ⇒ true
1522    | DATA _ ⇒ true
1523    | DATA16 _ ⇒ true
1524    | ACC_DPTR ⇒ true
1525    | ACC_PC ⇒ true
1526    | EXT_INDIRECT_DPTR ⇒ true
1527    | INDIRECT_DPTR ⇒ true
1528    | CARRY ⇒ true
1529    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1530    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1531    | RELATIVE _ ⇒ true
1532    | ADDR11 _ ⇒ true
1533    | ADDR16 _ ⇒ true ].
1534   
1535definition next_internal_pseudo_address_map0 ≝
1536  λT.
1537  λfetched.
1538  λM: internal_pseudo_address_map.
1539  λs: PreStatus T.
1540   match fetched with
1541    [ Comment _ ⇒ Some ? M
1542    | Cost _ ⇒ Some … M
1543    | Jmp _ ⇒ Some … M
1544    | Call _ ⇒
1545       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1546    | Mov _ _ ⇒ Some … M
1547    | Instruction instr ⇒
1548       match instr with
1549        [ ADD addr1 addr2 ⇒
1550           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1551            Some ? M
1552           else
1553            None ?
1554        | ADDC addr1 addr2 ⇒
1555           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1556            Some ? M
1557           else
1558            None ?
1559        | SUBB addr1 addr2 ⇒
1560           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1561            Some ? M
1562           else
1563            None ?       
1564        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1565 
1566
1567definition next_internal_pseudo_address_map ≝
1568 λM:internal_pseudo_address_map.
1569  λs:PseudoStatus.
1570    next_internal_pseudo_address_map0 ?
1571     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1572   
1573definition status_of_pseudo_status:
1574 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝
1575 λM,ps,pol.
1576  let pap ≝ code_memory … ps in
1577  let p ≝ assembly pap pol in
1578  let cm ≝ load_code_memory (\fst p) in
1579  let pc ≝ sigma pap pol (program_counter ? ps) in
1580  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1581  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1582     mk_PreStatus (BitVectorTrie Byte 16)
1583      cm
1584      lir
1585      hir
1586      (external_ram … ps)
1587      pc
1588      (special_function_registers_8051 … ps)
1589      (special_function_registers_8052 … ps)
1590      (p1_latch … ps)
1591      (p3_latch … ps)
1592      (clock … ps).
1593
1594(*
1595definition write_at_stack_pointer':
1596 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1597  λM: Type[0].
1598  λs: PreStatus M.
1599  λv: Byte.
1600    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1601    let bit_zero ≝ get_index_v… nu O ? in
1602    let bit_1 ≝ get_index_v… nu 1 ? in
1603    let bit_2 ≝ get_index_v… nu 2 ? in
1604    let bit_3 ≝ get_index_v… nu 3 ? in
1605      if bit_zero then
1606        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1607                              v (low_internal_ram ? s) in
1608          set_low_internal_ram ? s memory
1609      else
1610        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1611                              v (high_internal_ram ? s) in
1612          set_high_internal_ram ? s memory.
1613  [ cases l0 %
1614  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1615qed.
1616
1617definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1618 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1619
1620  λticks_of.
1621  λs.
1622  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1623  let ticks ≝ ticks_of (program_counter ? s) in
1624  let s ≝ set_clock ? s (clock ? s + ticks) in
1625  let s ≝ set_program_counter ? s pc in
1626    match instr with
1627    [ Instruction instr ⇒
1628       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1629    | Comment cmt ⇒ s
1630    | Cost cst ⇒ s
1631    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1632    | Call call ⇒
1633      let a ≝ address_of_word_labels s call in
1634      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1635      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1636      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1637      let s ≝ write_at_stack_pointer' ? s pc_bl in
1638      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1639      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1640      let s ≝ write_at_stack_pointer' ? s pc_bu in
1641        set_program_counter ? s a
1642    | Mov dptr ident ⇒
1643       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1644    ].
1645 [
1646 |2,3,4: %
1647 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1648 |
1649 | %
1650 ]
1651 cases not_implemented
1652qed.
1653*)
1654
1655axiom execute_1_pseudo_instruction_preserves_code_memory:
1656 ∀ticks_of,ps.
1657  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1658
1659(*
1660lemma execute_code_memory_unchanged:
1661 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1662 #ticks #ps whd in ⊢ (??? (??%))
1663 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1664  (program_counter pseudo_assembly_program ps)) #instr #pc
1665 whd in ⊢ (??? (??%)) cases instr
1666  [ #pre cases pre
1667     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1668       cases (split ????) #z1 #z2 %
1669     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1670       cases (split ????) #z1 #z2 %
1671     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1672       cases (split ????) #z1 #z2 %
1673     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1674       [ #x1 whd in ⊢ (??? (??%))
1675     | *: cases not_implemented
1676     ]
1677  | #comment %
1678  | #cost %
1679  | #label %
1680  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1681    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1682    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1683    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1684    (* CSC: ??? *)
1685  | #dptr #label (* CSC: ??? *)
1686  ]
1687  cases not_implemented
1688qed.
1689*)
1690
1691(* DEAD CODE?
1692lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1693 ∀M:internal_pseudo_address_map.
1694 ∀ps,ps': PseudoStatus.
1695 ∀pol.
1696  ∀prf:code_memory … ps = code_memory … ps'.
1697   let pol' ≝ ? in
1698   match status_of_pseudo_status M ps pol with
1699    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1700    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1701    ].
1702 [2: <prf @pol]
1703 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1704 generalize in match (refl … (assembly (code_memory … ps) pol))
1705 cases (assembly ??) in ⊢ (???% → %)
1706  [ #K whd whd in ⊢ (??%?) <H >K %
1707  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1708qed.
1709*)
1710
1711definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
1712  λprogram: pseudo_assembly_program.λpol.
1713  λppc: Word.
1714  λfetched.
1715    match fetched with
1716    [ Instruction instr ⇒
1717      match instr with
1718      [ JC lbl ⇒
1719        match pol ppc with
1720        [ short_jump ⇒ 〈2, 2〉
1721        | medium_jump ⇒ ?
1722        | long_jump ⇒ 〈4, 4〉
1723        ]
1724      | JNC lbl ⇒
1725        match pol ppc with
1726        [ short_jump ⇒ 〈2, 2〉
1727        | medium_jump ⇒ ?
1728        | long_jump ⇒ 〈4, 4〉
1729        ]
1730      | JB bit lbl ⇒
1731        match pol ppc with
1732        [ short_jump ⇒ 〈2, 2〉
1733        | medium_jump ⇒ ?
1734        | long_jump ⇒ 〈4, 4〉
1735        ]
1736      | JNB bit lbl ⇒
1737        match pol ppc with
1738        [ short_jump ⇒ 〈2, 2〉
1739        | medium_jump ⇒ ?
1740        | long_jump ⇒ 〈4, 4〉
1741        ]
1742      | JBC bit lbl ⇒
1743        match pol ppc with
1744        [ short_jump ⇒ 〈2, 2〉
1745        | medium_jump ⇒ ?
1746        | long_jump ⇒ 〈4, 4〉
1747        ]
1748      | JZ lbl ⇒
1749        match pol ppc with
1750        [ short_jump ⇒ 〈2, 2〉
1751        | medium_jump ⇒ ?
1752        | long_jump ⇒ 〈4, 4〉
1753        ]
1754      | JNZ lbl ⇒
1755        match pol ppc with
1756        [ short_jump ⇒ 〈2, 2〉
1757        | medium_jump ⇒ ?
1758        | long_jump ⇒ 〈4, 4〉
1759        ]
1760      | CJNE arg lbl ⇒
1761        match pol ppc with
1762        [ short_jump ⇒ 〈2, 2〉
1763        | medium_jump ⇒ ?
1764        | long_jump ⇒ 〈4, 4〉
1765        ]
1766      | DJNZ arg lbl ⇒
1767        match pol ppc with
1768        [ short_jump ⇒ 〈2, 2〉
1769        | medium_jump ⇒ ?
1770        | long_jump ⇒ 〈4, 4〉
1771        ]
1772      | ADD arg1 arg2 ⇒
1773        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1774         〈ticks, ticks〉
1775      | ADDC arg1 arg2 ⇒
1776        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1777         〈ticks, ticks〉
1778      | SUBB arg1 arg2 ⇒
1779        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1780         〈ticks, ticks〉
1781      | INC arg ⇒
1782        let ticks ≝ ticks_of_instruction (INC ? arg) in
1783         〈ticks, ticks〉
1784      | DEC arg ⇒
1785        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1786         〈ticks, ticks〉
1787      | MUL arg1 arg2 ⇒
1788        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1789         〈ticks, ticks〉
1790      | DIV arg1 arg2 ⇒
1791        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1792         〈ticks, ticks〉
1793      | DA arg ⇒
1794        let ticks ≝ ticks_of_instruction (DA ? arg) in
1795         〈ticks, ticks〉
1796      | ANL arg ⇒
1797        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1798         〈ticks, ticks〉
1799      | ORL arg ⇒
1800        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1801         〈ticks, ticks〉
1802      | XRL arg ⇒
1803        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1804         〈ticks, ticks〉
1805      | CLR arg ⇒
1806        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1807         〈ticks, ticks〉
1808      | CPL arg ⇒
1809        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1810         〈ticks, ticks〉
1811      | RL arg ⇒
1812        let ticks ≝ ticks_of_instruction (RL ? arg) in
1813         〈ticks, ticks〉
1814      | RLC arg ⇒
1815        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1816         〈ticks, ticks〉
1817      | RR arg ⇒
1818        let ticks ≝ ticks_of_instruction (RR ? arg) in
1819         〈ticks, ticks〉
1820      | RRC arg ⇒
1821        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1822         〈ticks, ticks〉
1823      | SWAP arg ⇒
1824        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1825         〈ticks, ticks〉
1826      | MOV arg ⇒
1827        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1828         〈ticks, ticks〉
1829      | MOVX arg ⇒
1830        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1831         〈ticks, ticks〉
1832      | SETB arg ⇒
1833        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1834         〈ticks, ticks〉
1835      | PUSH arg ⇒
1836        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1837         〈ticks, ticks〉
1838      | POP arg ⇒
1839        let ticks ≝ ticks_of_instruction (POP ? arg) in
1840         〈ticks, ticks〉
1841      | XCH arg1 arg2 ⇒
1842        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1843         〈ticks, ticks〉
1844      | XCHD arg1 arg2 ⇒
1845        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1846         〈ticks, ticks〉
1847      | RET ⇒
1848        let ticks ≝ ticks_of_instruction (RET ?) in
1849         〈ticks, ticks〉
1850      | RETI ⇒
1851        let ticks ≝ ticks_of_instruction (RETI ?) in
1852         〈ticks, ticks〉
1853      | NOP ⇒
1854        let ticks ≝ ticks_of_instruction (NOP ?) in
1855         〈ticks, ticks〉
1856      ]
1857    | Comment comment ⇒ 〈0, 0〉
1858    | Cost cost ⇒ 〈0, 0〉
1859    | Jmp jmp ⇒ 〈2, 2〉
1860    | Call call ⇒ 〈2, 2〉
1861    | Mov dptr tgt ⇒ 〈2, 2〉
1862    ].
1863  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1864qed.
1865
1866definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
1867  λprogram: pseudo_assembly_program.λpol.
1868  λppc: Word.
1869    let 〈preamble, pseudo〉 ≝ program in
1870    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1871     ticks_of0 program pol ppc fetched.
1872
1873lemma eq_rect_Type1_r:
1874  ∀A: Type[1].
1875  ∀a:A.
1876  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1877  #A #a #P #H #x #p
1878  generalize in match H
1879  generalize in match P
1880  cases p
1881  //
1882qed.
1883
1884axiom split_append:
1885  ∀A: Type[0].
1886  ∀m, n: nat.
1887  ∀v, v': Vector A m.
1888  ∀q, q': Vector A n.
1889    let 〈v', q'〉 ≝ split A m n (v@@q) in
1890      v = v' ∧ q = q'.
1891
1892axiom split_vector_singleton:
1893  ∀A: Type[0].
1894  ∀n: nat.
1895  ∀v: Vector A (S n).
1896  ∀rest: Vector A n.
1897  ∀s: Vector A 1.
1898  ∀prf.
1899    v = s @@ rest →
1900    ((get_index_v A ? v 0 prf) ::: rest) = v.
1901
1902example sub_minus_one_seven_eight:
1903  ∀v: BitVector 7.
1904  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1905  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1906 cases daemon.
1907qed.
1908
1909(*
1910lemma blah:
1911  ∀m: internal_pseudo_address_map.
1912  ∀s: PseudoStatus.
1913  ∀arg: Byte.
1914  ∀b: bool.
1915    addressing_mode_ok m s (DIRECT arg) = true →
1916      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1917      get_arg_8 ? s b (DIRECT arg).
1918  [2, 3: normalize % ]
1919  #m #s #arg #b #hyp
1920  whd in ⊢ (??%%)
1921  @split_elim''
1922  #nu' #nl' #arg_nu_nl_eq
1923  normalize nodelta
1924  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1925  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1926  #get_index_v_eq
1927  normalize nodelta
1928  [2:
1929    normalize nodelta
1930    @split_elim''
1931    #bit_one' #three_bits' #bit_one_three_bit_eq
1932    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1933    normalize nodelta
1934    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1935    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1936    #Saddr #carr' #Saddr_carr_eq
1937    normalize nodelta
1938    #carr_hyp'
1939    @carr_hyp'
1940    [1:
1941    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1942        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1943        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1944        #member_eq
1945        normalize nodelta
1946        [2: #destr destruct(destr)
1947        |1: -carr_hyp';
1948            >arg_nu_nl_eq
1949            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1950            [1: >get_index_v_eq in ⊢ (??%? → ?)
1951            |2: @le_S @le_S @le_S @le_n
1952            ]
1953            cases (member (BitVector 8) ? (\fst ?) ?)
1954            [1: #destr normalize in destr; destruct(destr)
1955            |2:
1956            ]
1957        ]
1958    |3: >get_index_v_eq in ⊢ (??%?)
1959        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1960        >(split_vector_singleton … bit_one_three_bit_eq)
1961        <arg_nu_nl_eq
1962        whd in hyp:(??%?)
1963        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1964        normalize nodelta [*: #ignore @sym_eq ]
1965    ]
1966  |
1967  ].
1968*)
1969(*
1970map_address0 ... (DIRECT arg) = Some .. →
1971  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1972  get_arg_8 (internal_ram ...) (DIRECT arg)
1973
1974((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1975                     then Some internal_pseudo_address_map M 
1976                     else None internal_pseudo_address_map )
1977                    =Some internal_pseudo_address_map M')
1978*)
1979
1980axiom low_internal_ram_write_at_stack_pointer:
1981 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1982  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
1983  low_internal_ram ? s2 = low_internal_ram T2 s3 →
1984  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
1985  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
1986  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
1987   low_internal_ram T1
1988     (write_at_stack_pointer ?
1989       (set_8051_sfr ?
1990         (write_at_stack_pointer ?
1991           (set_8051_sfr ?
1992             (set_low_internal_ram ? s1
1993               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
1994             SFR_SP sp1)
1995          bl)
1996        SFR_SP sp2)
1997      bu)
1998   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1999      (low_internal_ram ?
2000       (write_at_stack_pointer ?
2001         (set_8051_sfr ?
2002           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2003          SFR_SP sp2)
2004        pbu)).
2005
2006axiom high_internal_ram_write_at_stack_pointer:
2007 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2008  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2009  high_internal_ram ? s2 = high_internal_ram T2 s3 →
2010  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2011  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2012  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
2013   high_internal_ram T1
2014     (write_at_stack_pointer ?
2015       (set_8051_sfr ?
2016         (write_at_stack_pointer ?
2017           (set_8051_sfr ?
2018             (set_high_internal_ram ? s1
2019               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
2020             SFR_SP sp1)
2021          bl)
2022        SFR_SP sp2)
2023      bu)
2024   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2025      (high_internal_ram ?
2026       (write_at_stack_pointer ?
2027         (set_8051_sfr ?
2028           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2029          SFR_SP sp2)
2030        pbu)).
2031
2032lemma Some_Some_elim:
2033 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
2034 #T #x #y #P #H #K @H @option_destruct_Some //
2035qed.
2036
2037theorem main_thm:
2038 ∀M,M',ps,pol.
2039  next_internal_pseudo_address_map M ps = Some … M' →
2040   ∃n.
2041      execute n (status_of_pseudo_status M ps pol)
2042    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
2043 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
2044 #M #M' #ps #pol #SAFE
2045 cut
2046  (∀ps'.
2047    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
2048    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
2049 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
2050 #ps' #EQ
2051 whd in ⊢ (??(λ_.??(??%)?))
2052 change with
2053  (∃n.
2054    execute n
2055     (set_low_internal_ram ?
2056       (set_high_internal_ram ?
2057         (set_program_counter ?
2058           (set_code_memory ?? ps (load_code_memory ?))
2059          (sigma ? pol (program_counter ? ps)))
2060        (high_internal_ram_of_pseudo_high_internal_ram M ?))
2061      (low_internal_ram_of_pseudo_low_internal_ram M ?))
2062   = set_low_internal_ram ?
2063      (set_high_internal_ram ?
2064        (set_program_counter ?
2065          (set_code_memory ?? ? (load_code_memory ?))
2066         (sigma ???)) ?) ?)
2067 >EQ whd in match eq_rect_Type0_r normalize nodelta
2068 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
2069 generalize in match EQ -EQ;
2070 generalize in match (refl … (code_memory pseudo_assembly_program ps))
2071 generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
2072 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
2073 (* Dependent types madness ends here *)
2074 letin ppc ≝ (program_counter … ps)
2075 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
2076 letin assembled ≝ (\fst (assembly ? pol))
2077 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
2078 letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
2079 @pair_elim' #pi #newppc #EQ2
2080 letin instructions ≝
2081  (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
2082    (sigma ? pol ppc) (refl …) (refl …) (refl …))
2083 change with (fetch_many ???? → ?) #H1
2084 change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
2085 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
2086 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
2087 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
2088 generalize in match H1; -H1; generalize in match instructions -instructions
2089 * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi
2090 whd in match ticks_of normalize nodelta <EQ1 >EQ2
2091 cases pi in SAFE
2092  [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?)
2093   @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
2094   whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
2095   #H2 #EQ %[1,3:@0]
2096   <MAP >(eq_bv_eq … H2) >EQ %
2097  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
2098   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
2099       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
2100         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
2101         @pair_elim' * #instr #newppc' #ticks #EQ4       
2102         * * #H2a #H2b whd in ⊢ (% → ?) #H2
2103         >H2b >(eq_instruction_to_eq … H2a)
2104         #EQ %[@1]
2105         <MAP >(eq_bv_eq … H2) >EQ
2106         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
2107         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
2108         whd in ⊢ (??%?)
2109         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
2110         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2111  |6: (* Mov *) #arg1 #arg2
2112       #H1 #H2 #EQ %[@1]
2113       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2114       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2115       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2116       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2117       >H2b >(eq_instruction_to_eq … H2a)
2118       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2119       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2120       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2121       normalize nodelta;
2122       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2123       #result #flags
2124       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2125  |5: (* Call *) #label #MAP
2126      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
2127      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2128       [ (* short *) #abs @⊥ destruct (abs)
2129       |3: (* long *) #H1 #H2 #EQ %[@1]
2130           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2131           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2132           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2133           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2134           >H2b >(eq_instruction_to_eq … H2a)
2135           generalize in match EQ; -EQ;
2136           whd in ⊢ (???% → ??%?);
2137           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;
2138           >(eq_bv_eq … H2c)
2139           change with
2140            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
2141                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2142           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
2143           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;
2144           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
2145           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
2146           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
2147           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2148           @split_eq_status;
2149            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
2150              >code_memory_write_at_stack_pointer %
2151            | >set_program_counter_set_low_internal_ram
2152              >set_clock_set_low_internal_ram
2153              @low_internal_ram_write_at_stack_pointer
2154               [ >EQ0 @pol | % | %
2155               | @(pair_destruct_2 … EQ1)
2156               | @(pair_destruct_2 … EQ2)
2157               | >(pair_destruct_1 ????? EQpc)
2158                 >(pair_destruct_2 ????? EQpc)
2159                 @split_elim #x #y #H <H -x y H;
2160                 >(pair_destruct_1 ????? EQppc)
2161                 >(pair_destruct_2 ????? EQppc)
2162                 @split_elim #x #y #H <H -x y H;
2163                 >EQ0 % ]
2164            | >set_low_internal_ram_set_high_internal_ram
2165              >set_program_counter_set_high_internal_ram
2166              >set_clock_set_high_internal_ram
2167              @high_internal_ram_write_at_stack_pointer
2168               [ >EQ0 @pol | % | %
2169               | @(pair_destruct_2 … EQ1)
2170               | @(pair_destruct_2 … EQ2)
2171               | >(pair_destruct_1 ????? EQpc)
2172                 >(pair_destruct_2 ????? EQpc)
2173                 @split_elim #x #y #H <H -x y H;
2174                 >(pair_destruct_1 ????? EQppc)
2175                 >(pair_destruct_2 ????? EQppc)
2176                 @split_elim #x #y #H <H -x y H;
2177                 >EQ0 % ]           
2178            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
2179              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2180              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2181              >external_ram_write_at_stack_pointer %
2182            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
2183              >EQ0 %
2184            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
2185              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2186              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2187              >special_function_registers_8051_write_at_stack_pointer %
2188            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
2189              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2190              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2191              >special_function_registers_8052_write_at_stack_pointer %
2192            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
2193              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2194              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2195              >p1_latch_write_at_stack_pointer %
2196            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
2197              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2198              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2199              >p3_latch_write_at_stack_pointer %
2200            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
2201              >clock_write_at_stack_pointer whd in ⊢ (???%)
2202              >clock_write_at_stack_pointer whd in ⊢ (???%)
2203              >clock_write_at_stack_pointer %]
2204       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2205         @pair_elim' #fst_5_addr #rest_addr #EQ1
2206         @pair_elim' #fst_5_pc #rest_pc #EQ2
2207         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2208         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2209         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2210         change in ⊢ (? →??%?) with (execute_1_0 ??)
2211         @pair_elim' * #instr #newppc' #ticks #EQn
2212          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
2213          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2214          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
2215          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
2216          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
2217          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
2218          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
2219          >get_8051_sfr_set_8051_sfr
2220         
2221          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2222           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2223           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2224           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2225           generalize in match (refl … (split bool 4 4 pc_bu))
2226           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2227           generalize in match (refl … (split bool 3 8 rest_addr))
2228           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2229           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2230           generalize in match
2231            (refl …
2232             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2233             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2234           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2235           @split_eq_status try %
2236            [ change with (? = sigma ? (address_of_word_labels ps label))
2237              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2238            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2239              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
2240  |4: (* Jmp *) #label #MAP
2241      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
2242      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2243       [3: (* long *) #H1 #H2 #EQ %[@1]
2244           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2245           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2246           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2247           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2248           >H2b >(eq_instruction_to_eq … H2a)
2249           generalize in match EQ; -EQ;
2250           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2251           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2252       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2253           generalize in match
2254            (refl ?
2255             (sub_16_with_carry
2256              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
2257              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
2258              false))
2259           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2260           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2261           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2262           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2263           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2264           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2265           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2266           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2267           >H2b >(eq_instruction_to_eq … H2a)
2268           generalize in match EQ; -EQ;
2269           whd in ⊢ (???% → ?);
2270           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2271           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
2272           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
2273           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2274           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
2275           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2276       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2277         generalize in match
2278          (refl …
2279            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
2280         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2281         generalize in match
2282          (refl …
2283            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
2284         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2285         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2286         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2287         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2288         change in ⊢ (? →??%?) with (execute_1_0 ??)
2289           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2290           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2291           >H2b >(eq_instruction_to_eq … H2a)
2292           generalize in match EQ; -EQ;
2293           whd in ⊢ (???% → ?);
2294           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2295           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2296           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
2297           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2298           generalize in match (refl … (split bool 4 4 pc_bu))
2299           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2300           generalize in match (refl … (split bool 3 8 rest_addr))
2301           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2302           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2303           generalize in match
2304            (refl …
2305             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
2306             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2307           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
2308           @split_eq_status try %
2309            [ change with (? = sigma ?? (address_of_word_labels ps label))
2310              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2311            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2312              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2313  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
2314    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2315       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2316       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2317       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2318       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2319       >H2b >(eq_instruction_to_eq … H2a)
2320       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2321       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2322       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2323       normalize nodelta; #MAP;
2324       [1: change in ⊢ (? → %) with
2325        ((let 〈result,flags〉 ≝
2326          add_8_with_carry
2327           (get_arg_8 ? ps false ACC_A)
2328           (get_arg_8 ?
2329             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2330             false (DIRECT ARG2))
2331           ? in ?) = ?)
2332        [2,3: %]
2333        change in ⊢ (???% → ?) with
2334         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
2335        >get_arg_8_set_clock
2336       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
2337         [2,4: #abs @⊥ normalize in abs; destruct (abs)
2338         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
2339       [ change in ⊢ (? → %) with
2340        ((let 〈result,flags〉 ≝
2341          add_8_with_carry
2342           (get_arg_8 ? ps false ACC_A)
2343           (get_arg_8 ?
2344             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2345             false (DIRECT ARG2))
2346           ? in ?) = ?)
2347          >get_arg_8_set_low_internal_ram
2348       
2349        cases (add_8_with_carry ???)
2350         
2351        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2352       #result #flags
2353       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2354    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2355       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2356       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2357       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2358       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2359       >H2b >(eq_instruction_to_eq … H2a)
2360       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2361       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2362       [1,2,3,4: cases (half_add ???) #carry #result
2363       | cases (half_add ???) #carry #bl normalize nodelta;
2364         cases (full_add ????) #carry' #bu normalize nodelta ]
2365        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
2366        [5: %
2367        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2368      (set_program_counter pseudo_assembly_program ps newppc)
2369      (\fst  (ticks_of0 〈preamble,instr_list〉
2370                   (program_counter pseudo_assembly_program ps)
2371                   (Instruction (INC Identifier (DIRECT ARG))))
2372       +clock pseudo_assembly_program
2373        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2374        [2,3: // ]
2375            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2376            whd in ⊢ (??%%)
2377            cases (split bool 4 4 ARG)
2378            #nu' #nl'
2379            normalize nodelta
2380            cases (split bool 1 3 nu')
2381            #bit_1' #ignore'
2382            normalize nodelta
2383            cases (get_index_v bool 4 nu' ? ?)
2384            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2385            |
2386            ]
2387cases daemon (* EASY CASES TO BE COMPLETED *)
2388qed.
Note: See TracBrowser for help on using the repository browser.