root/src/ASM/AssemblyProof.ma @ 1952

Revision 1952, 70.0 KB (checked in by sacerdot, 12 months ago)

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