source: src/ASM/AssemblyProof.ma @ 2021

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

Proof skeleton in place. Several daemons to be closed adding invariants.

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