source: src/ASM/AssemblyProof.ma @ 1945

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

All proof statements repaired.

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