source: src/ASM/AssemblyProof.ma @ 1975

Last change on this file since 1975 was 1975, checked in by mulligan, 8 years ago

Work from today on closing main_thm.

File size: 76.0 KB
RevLine 
[877]1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
[1014]3include "ASM/StatusProofs.ma".
[1616]4include alias "arithmetics/nat.ma".
[877]5
[905]6definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
7  λP.
8    P true ∧ P false.
9 
10let rec bitvector_elim_prop_internal
[1936]11  (n: nat) (P: BitVector n → Prop) (m: nat)
12    on m:
13      m ≤ n → BitVector (n - m) → Prop ≝
[905]14  match m return λm. m ≤ n → BitVector (n - m) → Prop with
15  [ O    ⇒ λprf1. λprefix. P ?
[1936]16  | S n' ⇒ λprf2. λprefix.
17      bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
[905]18  ].
[1955]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
[905]24qed.
25
26definition bitvector_elim_prop ≝
27  λn: nat.
28  λP: BitVector n → Prop.
29    bitvector_elim_prop_internal n P n ? ?.
[1955]30  try @le_n
31  <minus_n_n @[[ ]]
[905]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
[1948]38  cases b cases c normalize nodelta
39  try (#_ % @I)
40  #assm destruct %
[905]41qed.
42
[877]43definition bit_elim: ∀P: bool → bool. bool ≝
44  λP.
45    P true ∧ P false.
46
47let rec bitvector_elim_internal
[1936]48  (n: nat) (P: BitVector n → bool) (m: nat)
49    on m:
50      m ≤ n → BitVector (n - m) → bool ≝
[877]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  ].
[1955]55  /2/
[877]56qed.
57
58definition bitvector_elim ≝
59  λn: nat.
60  λP: BitVector n → bool.
61    bitvector_elim_internal n P n ? ?.
[1941]62  try @le_n
63  <minus_n_n @[[]]
[877]64qed.
65
[992]66lemma super_rewrite2:
[1936]67  ∀A:Type[0].
68  ∀n, m: nat.
69  ∀v1: Vector A n.
70  ∀v2: Vector A m.
[992]71  ∀P: ∀m. Vector A m → Prop.
[1936]72    n = m → v1 ≃ v2 → P n v1 → P m v2.
[1939]73  #A #n #m #v1 #v2 #P #eq #jmeq
74  destruct #assm assumption
[992]75qed.
76
[877]77lemma vector_cons_append:
78  ∀A: Type[0].
79  ∀n: nat.
80  ∀e: A.
81  ∀v: Vector A n.
82    e ::: v = [[ e ]] @@ v.
[1936]83  #A #n #e #v
[1939]84  cases v try %
85  #n' #hd #tl %
[1936]86qed.
[877]87
[992]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
[1939]96  elim v try (#hd %)
97  #n' #hd' #tl' #ih #hd'
98  <ih %
[877]99qed.
100
[992]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)
[1936]111  try assumption %
[992]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.
[1936]120    (v @@ q) @@ r ≃ v @@ (q @@ r).
[992]121  #A #n #m #o #v #q #r
[1936]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
[992]128qed.
129
[877]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.
[1936]139  #A #m #o #eq #reflex #p #a
[1939]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
[877]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.
[1936]157  #A #m #o #eq #reflex #p #a
[1939]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
[877]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)).
[1936]175  #A #o #n #eq #reflex #h #v
[1939]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)
[1936]180  [1:
[1939]181    @mem_monotonic_wrt_append try assumption
182    @mem_monotonic_wrt_append try assumption
183    normalize >reflex %
[1936]184  |2:
[1939]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
[1936]191  ]
[877]192qed.
193
194lemma vector_cons_empty:
195  ∀A: Type[0].
196  ∀n: nat.
197  ∀v: Vector A n.
198    [[ ]] @@ v = v.
[1936]199  #A #n #v
200  cases v try %
201  #n' #hd #tl %
[877]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)).
[1936]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]])
[877]216qed.
217
218lemma eq_a_reflexive:
219  ∀a. eq_a a a = true.
[1936]220  #a cases a %
[877]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).
[1936]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
[877]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).
[1936]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
[877]253  ]
254qed.
255 
256let rec list_addressing_mode_tags_elim
[1936]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
[877]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 %
[1936]295  [2:
296    cases (sym_eq ??? prf); assumption
297  |1:
298    generalize in match H; generalize in match tl;
299    destruct #tl
[1616]300    normalize in ⊢ (∀_: %. ?);
[1936]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  ]
[877]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))).
[892]321
322(*                           
[877]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.
[892]404*)
[883]405(*definition eq_instruction ≝
[877]406  λi, j: instruction.
[883]407    true.*)
[885]408
[991]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.
[1936]491  #a
492  cases a try #arg1 try #arg2
493  try @eq_bv_refl try @eq_b_refl
[991]494  try normalize %
495qed.
496 
[1936]497definition eq_sum:
498    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
[991]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
[1939]741  cases s assumption
[991]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
[1936]752  cases s
753  whd in ⊢ (? → ? → ??%?);
754  #l #r
755  >leq_refl @req_refl
[991]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:
[1939]764    whd in ⊢ (??%?); try %
[991]765    >eq_addressing_mode_refl
766    >eq_addressing_mode_refl %
767  |13,15:
[1616]768    whd in ⊢ (??%?);
[991]769    cases arg1
770    [*:
771      #arg1_left normalize nodelta
772      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
773    ]
774  |11,12:
[1616]775    whd in ⊢ (??%?);
[991]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
[1939]787      >(eq_sum_refl …)
788      [1:
789        %
790      |2,3:
791        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
792      ]
[991]793    |4:
794      #arg1_left normalize nodelta
795      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
796    ]
797  |14:
[1616]798    whd in ⊢ (??%?);
[991]799    cases arg1
[1936]800    [1:
801      #arg1_left normalize nodelta
[991]802      @eq_sum_refl
[1936]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              ]
[991]819            ]
[1936]820          |2:
821            #arg @eq_prod_refl
822            [*:
823              #arg @eq_addressing_mode_refl
824            ]
[991]825          ]
[1936]826        |2:
827          #arg @eq_prod_refl
828          [*:
829            #arg @eq_addressing_mode_refl
830          ]
[991]831        ]
[1936]832      |2:
833        #arg @eq_prod_refl
834        [*:
835          #arg @eq_addressing_mode_refl
836        ]
[991]837      ]
[1936]838    |2:
839      #arg1_right normalize nodelta
840      @eq_prod_refl
841      [*:
842        #arg @eq_addressing_mode_refl
843      ]
[991]844    ]
845  |*:
[1616]846    whd in ⊢ (??%?);
[991]847    cases arg1
[1936]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        ]
[991]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.
[1941]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 %
[991]914qed.
915
[877]916let rec vect_member
[1936]917  (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A)
918    on v: bool ≝
[877]919  match v with
920  [ VEmpty          ⇒ false
921  | VCons len hd tl ⇒
[1936]922      eq hd a ∨ (vect_member A ? eq tl a)
[877]923  ].
[892]924
[877]925let rec list_addressing_mode_tags_elim_prop
926  (n: nat)
927  (l: Vector addressing_mode_tag (S n))
[884]928  on l:
929  ∀P: l → Prop.
[877]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
[884]939      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
[877]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. ?
[884]963  ] (refl ? (S n)). cases daemon. qed. (*
[877]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
[884]969    # SUB cases daemon ] qed.
[877]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.
[883]1051*)
[877]1052
[883]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
[1045]1058lemma split_zero:
1059  ∀A,m.
1060  ∀v: Vector A m.
1061    〈[[]], v〉 = split A 0 m v.
1062  #A #m #v
[1936]1063  cases v try %
1064  #n #hd #tl %
[1045]1065qed.
1066
[1936]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)
[1045]1076qed.
1077
[1936]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  ]
[1045]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
[1941]1110  destruct %
[1045]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
[1941]1118  destruct %
[1045]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
[1616]1127  generalize in match (Vector_O A q …);
[1941]1128  #hyp destruct %
[1045]1129qed.
1130
[1936]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.
[1045]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
[1936]1163  [1:
1164    #n #l #r #v #hd #eq #hyp
[1941]1165    destruct >(Vector_O … l) %
[1936]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))
[1941]1173    try (<hyp <head_head' %)
1174    elim l normalize //
[1936]1175  ]
1176qed.
[1045]1177
1178lemma split_prod:
[1936]1179  ∀A: Type[0].
1180  ∀m, n: nat.
[1045]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.
[1936]1185  #A #m elim m
1186  [1:
1187    #n #p #v #q #hyp
[1045]1188    >hyp <(vector_append_zero A n q v)
1189    >(prod_vector_zero_eq_left A …)
1190    @split_zero
[1936]1191  |2:
1192    #r #ih #n #p #v #q #hyp
[1045]1193    >hyp
[1936]1194    cases (Vector_Sn A r v) #hd #exists
1195    cases exists #tl #jmeq
[1941]1196    >jmeq @split_succ try %
[1936]1197    @ih %
[1045]1198  ]
1199qed.
1200
[1484]1201(*
[1045]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  ]
[1484]1217*)
[1045]1218
[1939]1219definition split_elim:
[1936]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.
[1939]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).
[1941]1230  λP. ?.
1231  cases daemon
1232qed.
[901]1233
1234(*
[883]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)))).
[894]1242 
[884]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.
[894]1251*)
[884]1252
[893]1253(*
[884]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.
[893]1258*)
[884]1259
[1936]1260let rec encoding_check
1261  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
1262    (encoding: list Byte)
1263      on encoding: Prop ≝
[890]1264  match encoding with
1265  [ nil ⇒ final_pc = pc
1266  | cons hd tl ⇒
1267    let 〈new_pc, byte〉 ≝ next code_memory pc in
[1484]1268      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
[890]1269  ].
1270
[1955]1271axiom add_commutative:
1272  ∀n: nat.
1273  ∀l, r: BitVector n.
1274    add n l r = add n r l.
1275
[1941]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
[1936]1281lemma encoding_check_append:
1282  ∀code_memory: BitVectorTrie Byte 16.
[1941]1283  ∀final_pc: Word.
[1936]1284  ∀l1: list Byte.
[1941]1285  ∀pc: Word.
[1936]1286  ∀l2: list Byte.
[1941]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.
[1936]1291  #code_memory #final_pc #l1 elim l1
1292  [1:
1293    #pc #l2
1294    whd in ⊢ (????% → ?); #H
[1941]1295    <add_zero
[1936]1296    whd whd in ⊢ (?%?); /2/
1297  |2:
1298    #hd #tl #IH #pc #l2 * #H1 #H2
[1946]1299(*    >add_SO in H2; #H2 *)
[1941]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    ]
[1936]1310  ]
[901]1311qed.
[890]1312
[1972]1313lemma destruct_bug_fix_1:
[1966]1314  ∀n: nat.
1315    S n = 0 → False.
1316  #n #absurd destruct(absurd)
[1955]1317qed.
1318
[1972]1319lemma destruct_bug_fix_2:
1320  ∀m, n: nat.
1321    S m = S n → m = n.
1322  #m #n #refl destruct %
1323qed.
1324
[1955]1325definition bitvector_3_cases:
[1941]1326  ∀b: BitVector 3.
[1955]1327    ∃l, c, r: bool.
[1966]1328      b ≃ [[l; c; r]].
[1955]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:
[1972]1332    #absurd @⊥ -b @(destruct_bug_fix_1 2)
[1955]1333    >absurd %
1334  |2:
[1966]1335    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
1336    cut (n = 2)
1337    [1:
[1972]1338      @destruct_bug_fix_2
1339      >size_refl %
[1966]1340    |2:
[1972]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    ]
[1955]1370  ]
1371qed.
[1941]1372
1373lemma bitvector_3_elim_prop:
[1936]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.
[1941]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
[1975]1382  cases l cases c cases r assumption
[1941]1383qed.
[894]1384
[936]1385definition ticks_of_instruction ≝
[1936]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 ?)).
[936]1390
[1041]1391lemma fetch_assembly:
[1941]1392  ∀pc: Word.
[1936]1393  ∀i: instruction.
1394  ∀code_memory: BitVectorTrie Byte 16.
1395  ∀assembled: list Byte.
[892]1396    assembled = assembly1 i →
[890]1397      let len ≝ length … assembled in
[1941]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.
[1936]1402  #pc #i #code_memory #assembled cases i [8: *]
[890]1403 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
[892]1404 [47,48,49:
1405 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
[890]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,
[892]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]
[1616]1414 normalize in ⊢ (???% → ?);
[897]1415 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
[1616]1416  normalize in ⊢ (???% → ?);]
1417 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
1418 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
[1649]1419 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
[1936]1420(*
1421 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
[897]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]
[1936]1426 whd >eq_instruction_refl >H4 @eq_bv_refl
1427*) (* XXX: not working! *)
[1041]1428qed.
[901]1429
[1936]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
[901]1435  [ nil ⇒ eq_bv … pc final_pc = true
1436  | cons i tl ⇒
[1936]1437    let fetched ≝ fetch code_memory pc in
1438    let 〈instr_pc, ticks〉 ≝ fetched in
1439    let 〈instr,pc'〉 ≝ instr_pc in
[936]1440      eq_instruction instr i = true ∧
[1936]1441        ticks = (ticks_of_instruction i) ∧
1442        fetch_many code_memory final_pc pc' tl
1443  ].
[901]1444
[1936]1445lemma option_destruct_Some:
1446  ∀A: Type[0].
1447  ∀a, b: A.
1448    Some A a = Some A b → a = b.
1449  #A #a #b #EQ
1450  destruct %
[892]1451qed.
[901]1452
[1975]1453lemma eq_instruction_to_eq:
[1936]1454  ∀i1, i2: instruction.
[1941]1455    eq_instruction i1 i2 = true → i1 ≃ i2.
[1975]1456  #i1 #i2
1457  cases i1 cases i2 cases daemon (*
1458  [1,10,19,28,37,46:
1459    #arg1 #arg2
1460    whd in match (eq_instruction ??);
1461    cases arg1 #subaddressing_mode
1462    cases subaddressing_mode
1463    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1464    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1465    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
1466    #word11 #irrelevant
1467    cases arg2 #subaddressing_mode
1468    cases subaddressing_mode
1469    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1470    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1471    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
1472    #word11' #irrelevant normalize nodelta
1473    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
1474qed.
[1936]1475         
[998]1476lemma fetch_assembly_pseudo':
[1936]1477  ∀lookup_labels.
[1948]1478  ∀sigma: Word → Word.
1479  ∀policy: Word → bool.
[1936]1480  ∀ppc.
1481  ∀lookup_datalabels.
1482  ∀pi.
1483  ∀code_memory.
1484  ∀len.
1485  ∀assembled.
1486  ∀instructions.
[1948]1487    let pc ≝ sigma ppc in
1488      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
1489        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
[1941]1490          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1491            encoding_check code_memory pc pc_plus_len assembled →
1492              fetch_many code_memory pc_plus_len pc instructions.
[1948]1493  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
1494  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
[1941]1495  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
1496  >len_refl >assembled_refl -len_refl
[1948]1497  generalize in match (add 16 (sigma ppc)
[1941]1498    (bitvector_of_nat 16
1499     (|flatten (Vector bool 8)
1500       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
1501  #final_pc
[1948]1502  generalize in match (sigma ppc); elim instructions
[1936]1503  [1:
1504    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
1505  |2:
[1941]1506    #i #tl #IH #pc #H whd
1507    cases (encoding_check_append ????? H) -H #H1 #H2
1508    @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta
1509    @pair_elim #instr #pc' #instr_pc_refl normalize nodelta
1510    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
1511    #H3 lapply (H3 H1) -H3 >fetch_refl >instr_pc_refl normalize nodelta
1512    #H3 lapply (conjunction_true ?? H3) * #H4 #H5 %
[1936]1513    [1:
[1941]1514      lapply (conjunction_true … H4) * #B1 #B2
1515      % try assumption @eqb_true_to_eq
1516      <(eq_instruction_to_eq … B1) assumption
[1936]1517    |2:
[1941]1518      >(eq_bv_eq … H5) @IH @H2
[1936]1519    ]
1520  ]
[901]1521qed.
1522
[998]1523lemma fetch_assembly_pseudo:
[1936]1524  ∀program: pseudo_assembly_program.
[1948]1525  ∀sigma: Word → Word.
1526  ∀policy: Word → bool.
1527  let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd  program) x) in
1528  ∀ppc.
1529  ∀code_memory.
[1649]1530  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
1531  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
[1948]1532  let pc ≝ sigma ppc in
1533  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1534  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
[1941]1535  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1536    encoding_check code_memory pc pc_plus_len assembled →
1537      fetch_many code_memory pc_plus_len pc instructions.
[1966]1538  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
1539  letin lookup_datalabels ≝ (λx.?)
1540  letin pi ≝ (fst ???)
1541  letin pc ≝ (sigma ?)
1542  letin instructions ≝ (expand_pseudo_instruction ??????)
1543  @pair_elim #len #assembled #assembled_refl normalize nodelta
1544  #H
1545  generalize in match
1546   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
1547  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
[877]1548qed.
1549
[1966]1550definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
1551  λpseudo_instruction.
1552    match pseudo_instruction with
1553    [ Comment c ⇒ False
1554    | Cost c ⇒ False
1555    | _ ⇒ True
1556    ].
1557
1558definition sigma_policy_specification ≝
1559  λprogram: pseudo_assembly_program.
1560  λsigma: Word → Word.
1561  λpolicy: Word → bool.
1562  ∀ppc: Word.
1563    let 〈preamble, instr_list〉 ≝ program in
1564    let pc ≝ sigma ppc in
1565    let labels ≝ \fst (create_label_cost_map instr_list) in
1566    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
1567    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc) in
1568    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
1569      And (nat_of_bitvector … ppc ≤ |instr_list| →
1570        next_pc = add 16 pc (bitvector_of_nat …
1571          (instruction_size lookup_labels sigma policy ppc instruction)))
1572       (Or (nat_of_bitvector … ppc < |instr_list| →
1573         nat_of_bitvector … pc < nat_of_bitvector … next_pc)
1574        (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
1575
[1941]1576(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
[1043]1577   function that load the code in memory is correct. The latter is based
1578   on missing properties from the standard library on the BitVectorTrie
[1941]1579   data structrure.
1580   
1581   Wrong at the moment, requires Jaap's precondition to ensure that the program
1582   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1583*)
[1957]1584lemma assembly_ok:
[1948]1585  ∀program.
1586  ∀sigma: Word → Word.
1587  ∀policy: Word → bool.
[1966]1588  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
[1948]1589  ∀assembled.
1590  ∀costs'.
[1957]1591  let 〈preamble, instr_list〉 ≝ program in
1592  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
[1966]1593  let datalabels ≝ construct_datalabels preamble in
1594  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1595    〈assembled,costs'〉 = assembly program sigma policy →
1596      costs = costs' ∧
1597        let code_memory ≝ load_code_memory assembled in
1598        let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 
1599          ∀ppc.
1600            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in     
1601            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1602            let pc ≝ sigma ppc in
1603            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1604              encoding_check code_memory pc pc_plus_len assembled ∧
1605                  sigma newppc = add … pc (bitvector_of_nat … len).
1606  #program #sigma #policy #sigma_policy_witness #assembled #costs'
[1957]1607  @pair_elim #preamble #instr_list #program_refl
1608  @pair_elim #labels #costs #create_label_cost_refl
[1966]1609  #assembly_refl % cases daemon (*
[1957]1610  [1:
[1966]1611    (* XXX: lemma on BitVectorTries *)
1612    cases daemon
1613  |2:
1614    #ppc #sigma_policy_specification_witness
1615    @pair_elim #pi #newppc #fetch_pseudo_refl
1616    cases pi
1617    [2,3: (* Cost and Comment cases *)
1618      #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd
1619    |1: (* PreInstruction cases *)
1620      #preinstruction #_
1621      @pair_elim #len #assembled' #assembly_1_pseudo_refl
1622      normalize nodelta %
[1957]1623      [1:
[1966]1624        cases assembled' normalize
[1957]1625      |2:
1626      ]
1627    ]
1628  ]
[1966]1629  cases daemon (* XXX: !!! *) *)
[1957]1630qed.
[906]1631
[1941]1632(* XXX: should we add that costs = costs'? *)
[1039]1633lemma fetch_assembly_pseudo2:
[1948]1634  ∀program.
1635  ∀sigma.
1636  ∀policy.
[1966]1637  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
[1948]1638  ∀ppc.
[1941]1639  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
[1948]1640  let 〈assembled, costs'〉 ≝ assembly program sigma policy in
[1014]1641  let code_memory ≝ load_code_memory assembled in
1642  let data_labels ≝ construct_datalabels (\fst program) in
[1948]1643  let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
[1649]1644  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
[1014]1645  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
[1948]1646  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1647    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
[1966]1648  * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc
[1941]1649  @pair_elim #labels #costs #create_label_map_refl
1650  @pair_elim #assembled #costs' #assembled_refl
1651  letin code_memory ≝ (load_code_memory ?)
1652  letin data_labels ≝ (construct_datalabels ?)
1653  letin lookup_labels ≝ (λx. ?)
1654  letin lookup_datalabels ≝ (λx. ?)
1655  @pair_elim #pi #newppc #fetch_pseudo_refl
[1966]1656  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs')
[1957]1657  normalize nodelta
[1941]1658  @pair_elim #labels' #costs' #create_label_map_refl' #H
1659  cases (H (sym_eq … assembled_refl))
1660  #_
[1948]1661  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1662  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
[1941]1663  #len #assembledi #EQ4 #H
1664  lapply (H ppc) >fetch_pseudo_refl #H
[1948]1665  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))
[1966]1666  >EQ4 #H1 cases H
1667  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
[1941]1668  >fetch_pseudo_refl in H1; #assm @assm assumption
[998]1669qed.
[985]1670
[906]1671(* OLD?
[877]1672definition assembly_specification:
1673  ∀assembly_program: pseudo_assembly_program.
1674  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1675  λpseudo_assembly_program.
1676  λcode_mem.
1677    ∀pc: Word.
1678      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1679      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1680      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1681      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1682      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1683       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1684      match pre_assembled with
1685       [ None ⇒ True
1686       | Some pc_code ⇒
1687          let 〈new_pc,code〉 ≝ pc_code in
1688           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1689
1690axiom assembly_meets_specification:
1691  ∀pseudo_assembly_program.
1692    match assembly pseudo_assembly_program with
1693    [ None ⇒ True
1694    | Some code_mem_cost ⇒
1695      let 〈code_mem, cost〉 ≝ code_mem_cost in
1696        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1697    ].
1698(*
1699  # PROGRAM
1700  [ cases PROGRAM
1701    # PREAMBLE
1702    # INSTR_LIST
1703    elim INSTR_LIST
1704    [ whd
1705      whd in ⊢ (∀_. %)
1706      # PC
1707      whd
1708    | # INSTR
1709      # INSTR_LIST_TL
1710      # H
1711      whd
1712      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1713    ]
1714  | cases not_implemented
1715  ] *)
[906]1716*)
[877]1717
[942]1718definition internal_pseudo_address_map ≝ list (BitVector 8).
1719
1720axiom low_internal_ram_of_pseudo_low_internal_ram:
1721 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1722
1723axiom high_internal_ram_of_pseudo_high_internal_ram:
1724 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1725
1726axiom low_internal_ram_of_pseudo_internal_ram_hit:
[1945]1727 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀addr:BitVector 7.
[942]1728  member ? (eq_bv 8) (false:::addr) M = true →
1729   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
[1666]1730   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
[1946]1731   let pbu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) (low_internal_ram … s) (zero 8) in
[942]1732   let bl ≝ lookup ? 7 addr ram (zero 8) in
[1946]1733   let bu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) ram (zero 8) in
[1945]1734    bu@@bl = \fst (sigma (pbu@@pbl)).
[942]1735
[949]1736(* changed from add to sub *)
[942]1737axiom low_internal_ram_of_pseudo_internal_ram_miss:
[1666]1738 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
[942]1739  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
[949]1740  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1741  let carr ≝ get_index_v ? ? flags 1 ? in
[942]1742  carr = false →
[949]1743  member ? (eq_bv 8) (false:::Saddr) M = false →
1744   member ? (eq_bv 8) (false:::addr) M = false →
1745    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1746  //
1747qed.
[942]1748
1749definition addressing_mode_ok ≝
[1666]1750 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
[942]1751  λaddr:addressing_mode.
1752   match addr with
1753    [ DIRECT d ⇒
1754       ¬(member ? (eq_bv 8) d M) ∧
1755       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1756    | INDIRECT i ⇒
[1666]1757       let d ≝ get_register … s [[false;false;i]] in
[942]1758       ¬(member ? (eq_bv 8) d M) ∧
1759       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1760    | EXT_INDIRECT _ ⇒ true
1761    | REGISTER _ ⇒ true
1762    | ACC_A ⇒ true
1763    | ACC_B ⇒ true
1764    | DPTR ⇒ true
1765    | DATA _ ⇒ true
1766    | DATA16 _ ⇒ true
1767    | ACC_DPTR ⇒ true
1768    | ACC_PC ⇒ true
1769    | EXT_INDIRECT_DPTR ⇒ true
1770    | INDIRECT_DPTR ⇒ true
1771    | CARRY ⇒ true
1772    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1773    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1774    | RELATIVE _ ⇒ true
1775    | ADDR11 _ ⇒ true
1776    | ADDR16 _ ⇒ true ].
[944]1777   
1778definition next_internal_pseudo_address_map0 ≝
[950]1779  λT.
[944]1780  λfetched.
1781  λM: internal_pseudo_address_map.
[1666]1782  λcm:T.
1783  λs: PreStatus T cm.
[944]1784   match fetched with
[942]1785    [ Comment _ ⇒ Some ? M
1786    | Cost _ ⇒ Some … M
1787    | Jmp _ ⇒ Some … M
1788    | Call _ ⇒
[1946]1789       Some … (add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1)::M)
[942]1790    | Mov _ _ ⇒ Some … M
1791    | Instruction instr ⇒
1792       match instr with
1793        [ ADD addr1 addr2 ⇒
[1666]1794           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
[942]1795            Some ? M
1796           else
1797            None ?
1798        | ADDC addr1 addr2 ⇒
[1666]1799           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
[942]1800            Some ? M
1801           else
1802            None ?
1803        | SUBB addr1 addr2 ⇒
[1666]1804           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
[942]1805            Some ? M
1806           else
1807            None ?       
1808        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
[944]1809 
1810
1811definition next_internal_pseudo_address_map ≝
1812 λM:internal_pseudo_address_map.
[1666]1813 λcm.
1814  λs:PseudoStatus cm.
[950]1815    next_internal_pseudo_address_map0 ?
[1666]1816     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s))) M cm s.
1817
1818definition code_memory_of_pseudo_assembly_program:
[1948]1819    ∀pap:pseudo_assembly_program.
1820      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1821  λpap.
1822  λsigma.
1823  λpolicy.
1824    let p ≝ assembly pap sigma policy in
1825      load_code_memory (\fst p).
[1666]1826
[942]1827definition status_of_pseudo_status:
[1948]1828    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1829      ∀sigma: Word → Word. ∀policy: Word → bool.
1830        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1831  λM.
1832  λpap.
1833  λps.
1834  λsigma.
1835  λpolicy.
1836  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1837  let pc ≝ sigma (program_counter … ps) in
[1014]1838  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1839  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1840     mk_PreStatus (BitVectorTrie Byte 16)
1841      cm
1842      lir
1843      hir
1844      (external_ram … ps)
1845      pc
1846      (special_function_registers_8051 … ps)
1847      (special_function_registers_8052 … ps)
1848      (p1_latch … ps)
1849      (p3_latch … ps)
1850      (clock … ps).
[877]1851
[909]1852(*
[877]1853definition write_at_stack_pointer':
1854 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1855  λM: Type[0].
1856  λs: PreStatus M.
1857  λv: Byte.
1858    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1859    let bit_zero ≝ get_index_v… nu O ? in
1860    let bit_1 ≝ get_index_v… nu 1 ? in
1861    let bit_2 ≝ get_index_v… nu 2 ? in
1862    let bit_3 ≝ get_index_v… nu 3 ? in
1863      if bit_zero then
1864        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1865                              v (low_internal_ram ? s) in
1866          set_low_internal_ram ? s memory
1867      else
1868        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1869                              v (high_internal_ram ? s) in
1870          set_high_internal_ram ? s memory.
1871  [ cases l0 %
1872  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1873qed.
1874
1875definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1876 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1877
1878  λticks_of.
1879  λs.
1880  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1881  let ticks ≝ ticks_of (program_counter ? s) in
1882  let s ≝ set_clock ? s (clock ? s + ticks) in
1883  let s ≝ set_program_counter ? s pc in
1884    match instr with
1885    [ Instruction instr ⇒
1886       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1887    | Comment cmt ⇒ s
1888    | Cost cst ⇒ s
1889    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1890    | Call call ⇒
1891      let a ≝ address_of_word_labels s call in
1892      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1893      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1894      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1895      let s ≝ write_at_stack_pointer' ? s pc_bl in
1896      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1897      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1898      let s ≝ write_at_stack_pointer' ? s pc_bu in
1899        set_program_counter ? s a
1900    | Mov dptr ident ⇒
1901       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1902    ].
1903 [
1904 |2,3,4: %
1905 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1906 |
1907 | %
1908 ]
1909 cases not_implemented
1910qed.
[909]1911*)
[911]1912
[877]1913(*
1914lemma execute_code_memory_unchanged:
1915 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1916 #ticks #ps whd in ⊢ (??? (??%))
1917 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1918  (program_counter pseudo_assembly_program ps)) #instr #pc
1919 whd in ⊢ (??? (??%)) cases instr
1920  [ #pre cases pre
1921     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1922       cases (split ????) #z1 #z2 %
1923     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1924       cases (split ????) #z1 #z2 %
1925     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1926       cases (split ????) #z1 #z2 %
1927     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1928       [ #x1 whd in ⊢ (??? (??%))
1929     | *: cases not_implemented
1930     ]
1931  | #comment %
1932  | #cost %
1933  | #label %
1934  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1935    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1936    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1937    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1938    (* CSC: ??? *)
1939  | #dptr #label (* CSC: ??? *)
1940  ]
1941  cases not_implemented
1942qed.
1943*)
1944
[1014]1945(* DEAD CODE?
[877]1946lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
[942]1947 ∀M:internal_pseudo_address_map.
[877]1948 ∀ps,ps': PseudoStatus.
[987]1949 ∀pol.
1950  ∀prf:code_memory … ps = code_memory … ps'.
1951   let pol' ≝ ? in
1952   match status_of_pseudo_status M ps pol with
1953    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1954    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
[877]1955    ].
[987]1956 [2: <prf @pol]
1957 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1958 generalize in match (refl … (assembly (code_memory … ps) pol))
1959 cases (assembly ??) in ⊢ (???% → %)
[877]1960  [ #K whd whd in ⊢ (??%?) <H >K %
1961  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
[909]1962qed.
[1014]1963*)
[877]1964
[1948]1965definition ticks_of0:
1966    ∀p:pseudo_assembly_program.
1967      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1968  λprogram: pseudo_assembly_program.
1969  λsigma.
1970  λpolicy.
[929]1971  λppc: Word.
[1953]1972  λfetched.
[929]1973    match fetched with
1974    [ Instruction instr ⇒
1975      match instr with
[1953]1976      [ JC lbl ⇒ ? (*
[1649]1977        match pol lookup_labels ppc with
[929]1978        [ short_jump ⇒ 〈2, 2〉
1979        | medium_jump ⇒ ?
1980        | long_jump ⇒ 〈4, 4〉
[1953]1981        ] *)
1982      | JNC lbl ⇒ ? (*
[1649]1983        match pol lookup_labels ppc with
[929]1984        [ short_jump ⇒ 〈2, 2〉
1985        | medium_jump ⇒ ?
1986        | long_jump ⇒ 〈4, 4〉
[1953]1987        ] *)
1988      | JB bit lbl ⇒ ? (*
[1649]1989        match pol lookup_labels ppc with
[929]1990        [ short_jump ⇒ 〈2, 2〉
1991        | medium_jump ⇒ ?
1992        | long_jump ⇒ 〈4, 4〉
[1953]1993        ] *)
1994      | JNB bit lbl ⇒ ? (*
[1649]1995        match pol lookup_labels ppc with
[929]1996        [ short_jump ⇒ 〈2, 2〉
1997        | medium_jump ⇒ ?
1998        | long_jump ⇒ 〈4, 4〉
[1953]1999        ] *)
2000      | JBC bit lbl ⇒ ? (*
[1649]2001        match pol lookup_labels ppc with
[929]2002        [ short_jump ⇒ 〈2, 2〉
2003        | medium_jump ⇒ ?
2004        | long_jump ⇒ 〈4, 4〉
[1953]2005        ] *)
2006      | JZ lbl ⇒ ? (*
[1649]2007        match pol lookup_labels ppc with
[929]2008        [ short_jump ⇒ 〈2, 2〉
2009        | medium_jump ⇒ ?
2010        | long_jump ⇒ 〈4, 4〉
[1953]2011        ] *)
2012      | JNZ lbl ⇒ ? (*
[1649]2013        match pol lookup_labels  ppc with
[929]2014        [ short_jump ⇒ 〈2, 2〉
2015        | medium_jump ⇒ ?
2016        | long_jump ⇒ 〈4, 4〉
[1953]2017        ] *)
2018      | CJNE arg lbl ⇒ ? (*
[1649]2019        match pol lookup_labels ppc with
[929]2020        [ short_jump ⇒ 〈2, 2〉
2021        | medium_jump ⇒ ?
2022        | long_jump ⇒ 〈4, 4〉
[1953]2023        ] *)
2024      | DJNZ arg lbl ⇒ ? (*
[1649]2025        match pol lookup_labels ppc with
[929]2026        [ short_jump ⇒ 〈2, 2〉
2027        | medium_jump ⇒ ?
2028        | long_jump ⇒ 〈4, 4〉
[1953]2029        ] *)
[936]2030      | ADD arg1 arg2 ⇒
2031        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
2032         〈ticks, ticks〉
[929]2033      | ADDC arg1 arg2 ⇒
[936]2034        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
2035         〈ticks, ticks〉
[929]2036      | SUBB arg1 arg2 ⇒
[936]2037        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
2038         〈ticks, ticks〉
[929]2039      | INC arg ⇒
[936]2040        let ticks ≝ ticks_of_instruction (INC ? arg) in
2041         〈ticks, ticks〉
[929]2042      | DEC arg ⇒
[936]2043        let ticks ≝ ticks_of_instruction (DEC ? arg) in
2044         〈ticks, ticks〉
[929]2045      | MUL arg1 arg2 ⇒
[936]2046        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
2047         〈ticks, ticks〉
[929]2048      | DIV arg1 arg2 ⇒
[936]2049        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
2050         〈ticks, ticks〉
[929]2051      | DA arg ⇒
[936]2052        let ticks ≝ ticks_of_instruction (DA ? arg) in
2053         〈ticks, ticks〉
[929]2054      | ANL arg ⇒
[936]2055        let ticks ≝ ticks_of_instruction (ANL ? arg) in
2056         〈ticks, ticks〉
[929]2057      | ORL arg ⇒
[936]2058        let ticks ≝ ticks_of_instruction (ORL ? arg) in
2059         〈ticks, ticks〉
[929]2060      | XRL arg ⇒
[936]2061        let ticks ≝ ticks_of_instruction (XRL ? arg) in
2062         〈ticks, ticks〉
[929]2063      | CLR arg ⇒
[936]2064        let ticks ≝ ticks_of_instruction (CLR ? arg) in
2065         〈ticks, ticks〉
[929]2066      | CPL arg ⇒
[936]2067        let ticks ≝ ticks_of_instruction (CPL ? arg) in
2068         〈ticks, ticks〉
[929]2069      | RL arg ⇒
[936]2070        let ticks ≝ ticks_of_instruction (RL ? arg) in
2071         〈ticks, ticks〉
[929]2072      | RLC arg ⇒
[936]2073        let ticks ≝ ticks_of_instruction (RLC ? arg) in
2074         〈ticks, ticks〉
[929]2075      | RR arg ⇒
[936]2076        let ticks ≝ ticks_of_instruction (RR ? arg) in
2077         〈ticks, ticks〉
[929]2078      | RRC arg ⇒
[936]2079        let ticks ≝ ticks_of_instruction (RRC ? arg) in
2080         〈ticks, ticks〉
[929]2081      | SWAP arg ⇒
[936]2082        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
2083         〈ticks, ticks〉
[929]2084      | MOV arg ⇒
[936]2085        let ticks ≝ ticks_of_instruction (MOV ? arg) in
2086         〈ticks, ticks〉
[929]2087      | MOVX arg ⇒
[936]2088        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
2089         〈ticks, ticks〉
[929]2090      | SETB arg ⇒
[936]2091        let ticks ≝ ticks_of_instruction (SETB ? arg) in
2092         〈ticks, ticks〉
[929]2093      | PUSH arg ⇒
[936]2094        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
2095         〈ticks, ticks〉
[929]2096      | POP arg ⇒
[936]2097        let ticks ≝ ticks_of_instruction (POP ? arg) in
2098         〈ticks, ticks〉
[929]2099      | XCH arg1 arg2 ⇒
[936]2100        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
2101         〈ticks, ticks〉
[929]2102      | XCHD arg1 arg2 ⇒
[936]2103        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
2104         〈ticks, ticks〉
[929]2105      | RET ⇒
[936]2106        let ticks ≝ ticks_of_instruction (RET ?) in
2107         〈ticks, ticks〉
[929]2108      | RETI ⇒
[936]2109        let ticks ≝ ticks_of_instruction (RETI ?) in
2110         〈ticks, ticks〉
[929]2111      | NOP ⇒
[936]2112        let ticks ≝ ticks_of_instruction (NOP ?) in
2113         〈ticks, ticks〉
[929]2114      ]
2115    | Comment comment ⇒ 〈0, 0〉
2116    | Cost cost ⇒ 〈0, 0〉
[938]2117    | Jmp jmp ⇒ 〈2, 2〉
2118    | Call call ⇒ 〈2, 2〉
2119    | Mov dptr tgt ⇒ 〈2, 2〉
[929]2120    ].
[1953]2121    cases daemon
2122qed.
[929]2123
[1948]2124definition ticks_of:
2125    ∀p:pseudo_assembly_program.
2126      (Word → Word) → (Word → bool) → Word → nat × nat ≝
2127  λprogram: pseudo_assembly_program.
2128  λsigma.
2129  λpolicy.
[936]2130  λppc: Word.
2131    let 〈preamble, pseudo〉 ≝ program in
2132    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
[1948]2133     ticks_of0 program sigma policy ppc fetched.
[930]2134
[935]2135lemma eq_rect_Type1_r:
2136  ∀A: Type[1].
[1948]2137  ∀a: A.
[935]2138  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2139  #A #a #P #H #x #p
[1649]2140  generalize in match H;
2141  generalize in match P;
[1948]2142  cases p //
[935]2143qed.
2144
[949]2145axiom split_append:
2146  ∀A: Type[0].
2147  ∀m, n: nat.
2148  ∀v, v': Vector A m.
2149  ∀q, q': Vector A n.
2150    let 〈v', q'〉 ≝ split A m n (v@@q) in
2151      v = v' ∧ q = q'.
2152
[1953]2153lemma split_vector_singleton:
[949]2154  ∀A: Type[0].
2155  ∀n: nat.
2156  ∀v: Vector A (S n).
2157  ∀rest: Vector A n.
2158  ∀s: Vector A 1.
2159    v = s @@ rest →
[1953]2160    ((get_index_v A ? v 0 ?) ::: rest) = v.
2161  [1:
2162    #A #n #v cases daemon (* XXX: !!! *)
2163  |2:
2164    @le_S_S @le_O_n
2165  ]
2166qed.
[949]2167
[985]2168example sub_minus_one_seven_eight:
[949]2169  ∀v: BitVector 7.
2170  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
2171  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
[985]2172 cases daemon.
2173qed.
[949]2174
[950]2175(*
[945]2176lemma blah:
[949]2177  ∀m: internal_pseudo_address_map.
[945]2178  ∀s: PseudoStatus.
2179  ∀arg: Byte.
[949]2180  ∀b: bool.
2181    addressing_mode_ok m s (DIRECT arg) = true →
2182      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2183      get_arg_8 ? s b (DIRECT arg).
2184  [2, 3: normalize % ]
2185  #m #s #arg #b #hyp
2186  whd in ⊢ (??%%)
2187  @split_elim''
2188  #nu' #nl' #arg_nu_nl_eq
2189  normalize nodelta
2190  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2191  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2192  #get_index_v_eq
2193  normalize nodelta
2194  [2:
2195    normalize nodelta
2196    @split_elim''
2197    #bit_one' #three_bits' #bit_one_three_bit_eq
2198    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2199    normalize nodelta
2200    generalize in match (refl ? (sub_7_with_carry ? ? ?))
2201    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2202    #Saddr #carr' #Saddr_carr_eq
2203    normalize nodelta
2204    #carr_hyp'
2205    @carr_hyp'
2206    [1:
2207    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2208        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2209        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2210        #member_eq
2211        normalize nodelta
2212        [2: #destr destruct(destr)
2213        |1: -carr_hyp';
2214            >arg_nu_nl_eq
2215            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2216            [1: >get_index_v_eq in ⊢ (??%? → ?)
2217            |2: @le_S @le_S @le_S @le_n
2218            ]
2219            cases (member (BitVector 8) ? (\fst ?) ?)
2220            [1: #destr normalize in destr; destruct(destr)
2221            |2:
2222            ]
2223        ]
2224    |3: >get_index_v_eq in ⊢ (??%?)
2225        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2226        >(split_vector_singleton … bit_one_three_bit_eq)
2227        <arg_nu_nl_eq
2228        whd in hyp:(??%?)
2229        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2230        normalize nodelta [*: #ignore @sym_eq ]
2231    ]
2232  |
2233  ].
[950]2234*)
[949]2235(*
[945]2236map_address0 ... (DIRECT arg) = Some .. →
2237  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2238  get_arg_8 (internal_ram ...) (DIRECT arg)
2239
2240((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
2241                     then Some internal_pseudo_address_map M 
2242                     else None internal_pseudo_address_map )
2243                    =Some internal_pseudo_address_map M')
[946]2244*)
[945]2245
[1014]2246axiom low_internal_ram_write_at_stack_pointer:
[1953]2247 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
2248 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
[1945]2249  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
[1666]2250  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
[1946]2251  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2252  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
[1953]2253  bu@@bl = sigma (pbu@@pbl) →
[1666]2254   low_internal_ram T1 cm1
2255     (write_at_stack_pointer …
2256       (set_8051_sfr …
2257         (write_at_stack_pointer …
2258           (set_8051_sfr …
2259             (set_low_internal_ram … s1
2260               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
[1014]2261             SFR_SP sp1)
2262          bl)
2263        SFR_SP sp2)
2264      bu)
2265   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
[1666]2266      (low_internal_ram …
2267       (write_at_stack_pointer …
2268         (set_8051_sfr …
2269           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
[1014]2270          SFR_SP sp2)
2271        pbu)).
2272
[1953]2273lemma high_internal_ram_write_at_stack_pointer:
2274 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
2275 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
[1945]2276  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
[1666]2277  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
[1946]2278  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2279  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
[1953]2280  bu@@bl = sigma (pbu@@pbl) →
[1666]2281   high_internal_ram T1 cm1
2282     (write_at_stack_pointer …
2283       (set_8051_sfr …
2284         (write_at_stack_pointer …
2285           (set_8051_sfr …
2286             (set_high_internal_ram … s1
2287               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
[1014]2288             SFR_SP sp1)
2289          bl)
2290        SFR_SP sp2)
2291      bu)
2292   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
[1666]2293      (high_internal_ram …
2294       (write_at_stack_pointer …
2295         (set_8051_sfr …
2296           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
[1014]2297          SFR_SP sp2)
2298        pbu)).
[1953]2299  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
2300  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
2301  cases daemon (* XXX: !!! *)
2302qed.
[1014]2303
[1037]2304lemma Some_Some_elim:
2305 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
2306 #T #x #y #P #H #K @H @option_destruct_Some //
2307qed.
2308
[1957]2309lemma pair_destruct_right:
2310  ∀A: Type[0].
2311  ∀B: Type[0].
2312  ∀a, c: A.
2313  ∀b, d: B.
2314    〈a, b〉 = 〈c, d〉 → b = d.
2315  #A #B #a #b #c #d //
2316qed.
[1955]2317   
[1945]2318(*CSC: ???*)
[1953]2319lemma snd_assembly_1_pseudoinstruction_ok:
[1948]2320  ∀program: pseudo_assembly_program.
2321  ∀sigma: Word → Word.
2322  ∀policy: Word → bool.
[1966]2323  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
[1948]2324  ∀ppc: Word.
2325  ∀pi.
2326  ∀lookup_labels.
2327  ∀lookup_datalabels.
2328    lookup_labels = (λx. sigma (address_of_word_labels_code_mem (\snd program) x)) →
2329    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
2330    \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
[1955]2331    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels  pi) in
[1948]2332      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
[1966]2333  #program #sigma #policy #sigma_policy_specification_witness #ppc #pi
2334  #lookup_labels #lookup_datalabels
2335  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
[1955]2336  normalize nodelta
2337  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
2338  #fetch_pseudo_refl
2339  letin assembled ≝ (\fst (assembly program sigma policy))
2340  letin costs ≝ (\snd (assembly program sigma policy))
[1966]2341  lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
[1957]2342  @pair_elim #preamble #instr_list #program_refl
[1955]2343  @pair_elim #labels #costs' #create_label_cost_map_refl
2344  <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
2345  lapply (H ppc) -H
2346  @pair_elim #pi' #newppc #fetch_pseudo_refl'
[1966]2347  @pair_elim #len #assembled #assembly1_refl #H
2348  cases H
[1955]2349  #encoding_check_assm #sigma_newppc_refl
2350  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
2351  >pi_refl' in assembly1_refl; #assembly1_refl
[1966]2352  >lookup_labels_refl >lookup_datalabels_refl
2353  >program_refl normalize nodelta
2354  >assembly1_refl
[1955]2355  <sigma_newppc_refl
2356  generalize in match fetch_pseudo_refl';
2357  whd in match (fetch_pseudo_instruction ??);
2358  @pair_elim #lbl #instr #nth_refl normalize nodelta
[1957]2359  #G cases (pair_destruct_right ?????? G) %
[1953]2360qed.
[1667]2361
2362lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
[1948]2363  /2/
[1667]2364qed.
2365
[1668]2366(* To be moved in ProofStatus *)
2367lemma program_counter_set_program_counter:
[1948]2368  ∀T.
2369  ∀cm.
2370  ∀s.
2371  ∀x.
2372    program_counter T cm (set_program_counter T cm s x) = x.
2373  //
[1668]2374qed.
Note: See TracBrowser for help on using the repository browser.