source: src/ASM/AssemblyProof.ma @ 1936

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

Some holes filled in AssemblyProof?.ma.

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