source: src/ASM/AssemblyProof.ma @ 1939

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

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

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