source: src/ASM/AssemblyProof.ma @ 905

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

work from today

File size: 54.6 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4(* RUSSEL **)
5
6include "basics/jmeq.ma".
7
8notation > "hvbox(a break ≃ b)"
9  non associative with precedence 45
10for @{ 'jmeq ? $a ? $b }.
11
12notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
13  non associative with precedence 45
14for @{ 'jmeq $t $a $u $b }.
15
16interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
17
18lemma eq_to_jmeq:
19  ∀A: Type[0].
20  ∀x, y: A.
21    x = y → x ≃ y.
22  //
23qed.
24
25definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
26definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
27
28coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
29coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
30
31axiom VOID: Type[0].
32axiom assert_false: VOID.
33definition bigbang: ∀A:Type[0].False → VOID → A.
34 #A #abs cases abs
35qed.
36
37coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
38
39lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
40 #A #P #p cases p #w #q @q
41qed.
42
43lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
44 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
45qed.
46
47coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
48
49(* END RUSSELL **)
50
51
52definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
53  λP.
54    P true ∧ P false.
55 
56let rec bitvector_elim_prop_internal
57  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
58  match m return λm. m ≤ n → BitVector (n - m) → Prop with
59  [ O    ⇒ λprf1. λprefix. P ?
60  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
61  ].
62  [ applyS prefix
63  | letin res ≝ (bit ::: prefix)
64    < (minus_S_S ? ?)
65    > (minus_Sn_m ? ?)
66  [ @ res
67  | @ prf2
68  ]
69  | /2/
70  ].
71qed.
72
73definition bitvector_elim_prop ≝
74  λn: nat.
75  λP: BitVector n → Prop.
76    bitvector_elim_prop_internal n P n ? ?.
77  [ @ (le_n ?)
78  | < (minus_n_n ?)
79    @ [[ ]]
80  ]
81qed.
82
83lemma eq_b_eq:
84  ∀b, c.
85    eq_b b c = true → b = c.
86  #b #c
87  cases b
88  cases c
89  normalize //
90qed.
91
92lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
93 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
94 #n #hd #tl #abs @⊥ //
95qed.
96
97lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
98 ∃hd.∃tl.v ≃ VCons bool n hd tl.
99 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
100 [ #abs @⊥ //
101 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
102qed.
103
104lemma eq_bv_eq:
105  ∀n, v, q.
106    eq_bv n v q = true → v = q.
107  #n #v #q generalize in match v
108  elim q
109  [ #v #h @BitVector_O
110  | #n #hd #tl #ih #v' #h
111    cases (BitVector_Sn ? v')
112    #hd' * #tl' #jmeq >jmeq in h;
113    #new_h
114    change in new_h with ((andb ? ?) = ?);
115    cases(conjunction_true … new_h)
116    #eq_heads #eq_tails
117    whd in eq_heads:(??(??(%))?);
118    cases(eq_b_eq … eq_heads)
119    whd in eq_tails:(??(?????(%))?);
120    change in eq_tails with (eq_bv ??? = ?);
121    <(ih tl') //
122  ]
123qed.
124
125lemma bool_eq_internal_eq:
126  ∀b, c.
127    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
128  #b #c
129  cases b
130  [ normalize //
131  | normalize
132    cases c
133    [ normalize //
134    | normalize //
135    ]
136  ]
137qed.
138
139lemma eq_bv_refl:
140  ∀n,v. eq_bv n v v = true.
141  #n #v
142  elim v
143  [ //
144  | #n #hd #tl #ih
145    normalize
146    cases hd
147    [ normalize
148      @ ih
149    | normalize
150      @ ih
151    ]
152  ]
153qed.
154
155lemma eq_eq_bv:
156  ∀n, v, q.
157    v = q → eq_bv n v q = true.
158  #n #v
159  elim v
160  [ #q #h <h normalize %
161  | #n #hd #tl #ih #q #h >h //
162  ]
163qed.
164
165let rec foldl_strong_internal
166  (A: Type[0]) (P: list A → Type[0]) (l: list A)
167  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
168  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
169    l = prefix @ suffix → P(prefix @ suffix) ≝
170  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
171  [ nil ⇒ λprf. ?
172  | cons hd tl ⇒ λprf. ?
173  ].
174  [ > (append_nil ?)
175    @ acc
176  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
177    [ @ (H prefix hd tl prf acc)
178    | applyS prf
179    ]
180  ]
181qed.
182
183definition foldl_strong ≝
184  λA: Type[0].
185  λP: list A → Type[0].
186  λl: list A.
187  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
188  λacc: P [ ].
189    foldl_strong_internal A P l H [ ] l acc (refl …).
190
191definition bit_elim: ∀P: bool → bool. bool ≝
192  λP.
193    P true ∧ P false.
194
195let rec bitvector_elim_internal
196  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
197  match m return λm. m ≤ n → BitVector (n - m) → bool with
198  [ O    ⇒ λprf1. λprefix. P ?
199  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
200  ].
201  [ applyS prefix
202  | letin res ≝ (bit ::: prefix)
203    < (minus_S_S ? ?)
204    > (minus_Sn_m ? ?)
205    [ @ res
206    | @ prf2
207    ]
208  | /2/
209  ].
210qed.
211
212definition bitvector_elim ≝
213  λn: nat.
214  λP: BitVector n → bool.
215    bitvector_elim_internal n P n ? ?.
216  [ @ (le_n ?)
217  | < (minus_n_n ?)
218    @ [[ ]]
219  ]
220qed.
221
222axiom vector_associative_append:
223  ∀A: Type[0].
224  ∀n, m, o:  nat.
225  ∀v: Vector A n.
226  ∀q: Vector A m.
227  ∀r: Vector A o.
228    ((v @@ q) @@ r)
229    ≃
230    (v @@ (q @@ r)).
231       
232lemma vector_cons_append:
233  ∀A: Type[0].
234  ∀n: nat.
235  ∀e: A.
236  ∀v: Vector A n.
237    e ::: v = [[ e ]] @@ v.
238  # A # N # E # V
239  elim V
240  [ normalize %
241  | # NN # AA # VV # IH
242    normalize
243    %
244  ]
245qed.
246
247lemma super_rewrite2:
248 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
249  ∀P: ∀m. Vector A m → Prop.
250   n=m → v1 ≃ v2 → P n v1 → P m v2.
251 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
252qed.
253
254lemma mem_middle_vector:
255  ∀A: Type[0].
256  ∀m, o: nat.
257  ∀eq: A → A → bool.
258  ∀reflex: ∀a. eq a a = true.
259  ∀p: Vector A m.
260  ∀a: A.
261  ∀r: Vector A o.
262    mem A eq ? (p@@(a:::r)) a = true.
263  # A # M # O # EQ # REFLEX # P # A
264  elim P
265  [ normalize
266    > (REFLEX A)
267    normalize
268    # H
269    %
270  | # NN # AA # PP # IH
271    normalize
272    cases (EQ A AA) //
273     @ IH
274  ]
275qed.
276
277lemma mem_monotonic_wrt_append:
278  ∀A: Type[0].
279  ∀m, o: nat.
280  ∀eq: A → A → bool.
281  ∀reflex: ∀a. eq a a = true.
282  ∀p: Vector A m.
283  ∀a: A.
284  ∀r: Vector A o.
285    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
286  # A # M # O # EQ # REFLEX # P # A
287  elim P
288  [ #R #H @H
289  | #NN #AA # PP # IH #R #H
290    normalize
291    cases (EQ A AA)
292    [ normalize %
293    | @ IH @ H
294    ]
295  ]
296qed.
297
298lemma subvector_multiple_append:
299  ∀A: Type[0].
300  ∀o, n: nat.
301  ∀eq: A → A → bool.
302  ∀refl: ∀a. eq a a = true.
303  ∀h: Vector A o.
304  ∀v: Vector A n.
305  ∀m: nat.
306  ∀q: Vector A m.
307    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
308  # A # O # N # EQ # REFLEX # H # V
309  elim V
310  [ normalize
311    # M # V %
312  | # NN # AA # VV # IH # MM # QQ
313    change with (bool_to_Prop (andb ??))
314    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
315    [
316    | # HH > HH
317      > (vector_cons_append ? ? AA VV)
318      change with (bool_to_Prop (subvector_with ??????))
319      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
320        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
321        ?
322        (vector_associative_append A ? ? ? QQ [[AA]] VV))
323      [ >associative_plus //
324      | @IH ]
325    ]
326    @(mem_monotonic_wrt_append)
327    [ @ REFLEX
328    | @(mem_monotonic_wrt_append)
329      [ @ REFLEX
330      | normalize
331        > REFLEX
332        normalize
333        %
334      ]
335    ]
336qed.
337
338lemma vector_cons_empty:
339  ∀A: Type[0].
340  ∀n: nat.
341  ∀v: Vector A n.
342    [[ ]] @@ v = v.
343  # A # N # V
344  elim V
345  [ normalize %
346  | # NN # HH # VV #H %
347  ]
348qed.
349
350corollary subvector_hd_tl:
351  ∀A: Type[0].
352  ∀o: nat.
353  ∀eq: A → A → bool.
354  ∀refl: ∀a. eq a a = true.
355  ∀h: A.
356  ∀v: Vector A o.
357    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
358  # A # O # EQ # REFLEX # H # V
359  > (vector_cons_append A ? H V)
360  < (vector_cons_empty A ? ([[H]] @@ V))
361  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
362qed.
363
364lemma eq_a_reflexive:
365  ∀a. eq_a a a = true.
366  # A
367  cases A
368  %
369qed.
370
371lemma is_in_monotonic_wrt_append:
372  ∀m, n: nat.
373  ∀p: Vector addressing_mode_tag m.
374  ∀q: Vector addressing_mode_tag n.
375  ∀to_search: addressing_mode.
376    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
377  # M # N # P # Q # TO_SEARCH
378  # H
379  elim Q
380  [ normalize
381    @ H
382  | # NN # PP # QQ # IH
383    normalize
384    cases (is_a PP TO_SEARCH)
385    [ normalize
386      %
387    | normalize
388      normalize in IH
389      @ IH
390    ]
391  ]
392qed.
393
394corollary is_in_hd_tl:
395  ∀to_search: addressing_mode.
396  ∀hd: addressing_mode_tag.
397  ∀n: nat.
398  ∀v: Vector addressing_mode_tag n.
399    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
400  # TO_SEARCH # HD # N # V
401  elim V
402  [ # H
403    normalize in H;
404    cases H
405  | # NN # HHD # VV # IH # HH
406    > vector_cons_append
407    > (vector_cons_append ? ? HHD VV)
408    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
409    @ HH
410  ]
411qed.
412 
413let rec list_addressing_mode_tags_elim
414  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
415  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
416   (l → bool) → bool ] with
417  [ VEmpty      ⇒  true 
418  | VCons len hd tl ⇒ λP.
419    let process_hd ≝
420      match hd return λhd. ∀P: hd:::tl → bool. bool with
421      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
422      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
423      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
424      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
425      | acc_a ⇒ λP.P ACC_A
426      | acc_b ⇒ λP.P ACC_B
427      | dptr ⇒ λP.P DPTR
428      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
429      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
430      | acc_dptr ⇒ λP.P ACC_DPTR
431      | acc_pc ⇒ λP.P ACC_PC
432      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
433      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
434      | carry ⇒ λP.P CARRY
435      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
436      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
437      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
438      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
439      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
440      ]
441    in
442      andb (process_hd P)
443       (match len return λx. x = len → bool with
444         [ O ⇒ λprf. true
445         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
446  ].
447  try %
448  [ 2: cases (sym_eq ??? prf); @tl
449  | generalize in match H; generalize in match tl; cases prf;
450    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
451    #tl
452    normalize in ⊢ (∀_: %. ?)
453    # H
454    whd
455    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
456    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
457qed.
458
459definition product_elim ≝
460  λm, n: nat.
461  λv: Vector addressing_mode_tag (S m).
462  λq: Vector addressing_mode_tag (S n).
463  λP: (v × q) → bool.
464    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
465
466definition union_elim ≝
467  λA, B: Type[0].
468  λelimA: (A → bool) → bool.
469  λelimB: (B → bool) → bool.
470  λelimU: A ⊎ B → bool.
471    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
472
473(*                           
474definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
475  λP.
476    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
477    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
478    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
479    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
480    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
481    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
482    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
483    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
484    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
485    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
486    P (DA ? ACC_A) ∧
487    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
488    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
489    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
490    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
491    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
492    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
493    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
494    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
495    P (RL ? ACC_A) ∧
496    P (RLC ? ACC_A) ∧
497    P (RR ? ACC_A) ∧
498    P (RRC ? ACC_A) ∧
499    P (SWAP ? ACC_A) ∧
500    P (RET ?) ∧
501    P (RETI ?) ∧
502    P (NOP ?) ∧
503    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
504    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
505    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
506    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
507    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
508                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
509                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
510    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
511    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
512                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
513                   (λd. P (XRL ? d)) ∧
514    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
515                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
516                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
517                   (λd. P (ANL ? d)) ∧
518    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
519                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
520                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
521                   (λd. P (ORL ? d)) ∧
522    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
523                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
524                   (λd. P (MOVX ? d)) ∧
525    union_elim ? ? (
526      union_elim ? ? (
527        union_elim ? ? (
528          union_elim ? ? (
529            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
530                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
531                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
532                            (product_elim ? ? [[dptr]] [[data16]]))
533                            (product_elim ? ? [[carry]] [[bit_addr]]))
534                            (product_elim ? ? [[bit_addr]] [[carry]])
535                            (λd. P (MOV ? d)).
536  %
537qed.
538 
539definition instruction_elim: ∀P: instruction → bool. bool ≝
540  λP. (*
541    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
542    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
543    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
544    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
545    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
546    P (JMP INDIRECT_DPTR) ∧
547    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
548    preinstruction_elim (λp. P (RealInstruction p)). *)
549  %
550qed.
551
552
553axiom instruction_elim_complete:
554 ∀P. instruction_elim P = true → ∀i. P i = true.
555*)
556(*definition eq_instruction ≝
557  λi, j: instruction.
558    true.*)
559axiom eq_instruction: instruction → instruction → bool.
560axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
561
562let rec vect_member
563  (A: Type[0]) (n: nat) (eq: A → A → bool)
564  (v: Vector A n) (a: A) on v: bool ≝
565  match v with
566  [ VEmpty          ⇒ false
567  | VCons len hd tl ⇒
568    eq hd a ∨ (vect_member A ? eq tl a)
569  ].
570
571let rec list_addressing_mode_tags_elim_prop
572  (n: nat)
573  (l: Vector addressing_mode_tag (S n))
574  on l:
575  ∀P: l → Prop.
576  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
577  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
578  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
579  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
580  ∀x: l. P x ≝
581  match l return
582    λy.
583      match y with
584      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
585      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
586               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
587               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
588               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
589               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
590               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
591               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
592               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
593               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
594               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
595               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
596               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
597               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
598               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
599               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
600               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
601               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
602               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
603               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
604               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
605               ∀x:l. P x
606      ] with
607  [ VEmpty          ⇒ λAbsurd. ⊥
608  | VCons len hd tl ⇒ λProof. ?
609  ] (refl ? (S n)). cases daemon. qed. (*
610  [ destruct(Absurd)
611  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
612    # A8 # A9 # A10 # A11 # A12 # A13 # A14
613    # A15 # A16 # A17 # A18 # A19 # X
614    cases X
615    # SUB cases daemon ] qed.
616    cases SUB
617    [ # BYTE
618    normalize
619  ].
620 
621 
622(*    let prepare_hd ≝
623      match hd with
624      [ direct ⇒ λdirect_prf. ?
625      | indirect ⇒ λindirect_prf. ?
626      | ext_indirect ⇒ λext_indirect_prf. ?
627      | registr ⇒ λregistr_prf. ?
628      | acc_a ⇒ λacc_a_prf. ?
629      | acc_b ⇒ λacc_b_prf. ?
630      | dptr ⇒ λdptr_prf. ?
631      | data ⇒ λdata_prf. ?
632      | data16 ⇒ λdata16_prf. ?
633      | acc_dptr ⇒ λacc_dptr_prf. ?
634      | acc_pc ⇒ λacc_pc_prf. ?
635      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
636      | indirect_dptr ⇒ λindirect_prf. ?
637      | carry ⇒ λcarry_prf. ?
638      | bit_addr ⇒ λbit_addr_prf. ?
639      | n_bit_addr ⇒ λn_bit_addr_prf. ?
640      | relative ⇒ λrelative_prf. ?
641      | addr11 ⇒ λaddr11_prf. ?
642      | addr16 ⇒ λaddr16_prf. ?
643      ]
644    in ? *)
645  ].
646  [ 1: destruct(absd)
647  | 2: # A1 # A2 # A3 # A4 # A5 # A6
648       # A7 # A8 # A9 # A10 # A11 # A12
649       # A13 # A14 # A15 # A16 # A17 # A18
650       # A19 *
651  ].
652
653
654  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
655   (l → bool) → bool ] with
656  [ VEmpty      ⇒  true 
657  | VCons len hd tl ⇒ λP.
658    let process_hd ≝
659      match hd return λhd. ∀P: hd:::tl → bool. bool with
660      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
661      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
662      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
663      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
664      | acc_a ⇒ λP.P ACC_A
665      | acc_b ⇒ λP.P ACC_B
666      | dptr ⇒ λP.P DPTR
667      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
668      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
669      | acc_dptr ⇒ λP.P ACC_DPTR
670      | acc_pc ⇒ λP.P ACC_PC
671      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
672      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
673      | carry ⇒ λP.P CARRY
674      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
675      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
676      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
677      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
678      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
679      ]
680    in
681      andb (process_hd P)
682       (match len return λx. x = len → bool with
683         [ O ⇒ λprf. true
684         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
685  ].
686  try %
687  [ 2: cases (sym_eq ??? prf); @tl
688  | generalize in match H; generalize in match tl; cases prf;
689    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
690    #tl
691    normalize in ⊢ (∀_: %. ?)
692    # H
693    whd
694    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
695    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
696qed.
697*)
698(*
699lemma test:
700  let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
701      (let assembled ≝ assembly1 i in
702      let code_memory ≝ load_code_memory assembled in
703      let fetched ≝ fetch code_memory ? in
704      let 〈instr_pc, ticks〉 ≝ fetched in
705        eq_instruction (\fst instr_pc)) i = true.
706 [2: @ zero
707 | normalize
708 ]*)
709
710lemma BitVectorTrie_O:
711 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
712 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
713  [ #w #_ %1 %[@w] %
714  | #n #l #r #abs @⊥ //
715  | #n #EQ %2 >EQ %]
716qed.
717
718lemma BitVectorTrie_Sn:
719 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
720 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
721  [ #m #abs @⊥ //
722  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
723  | #m #EQ %2 // ]
724qed.
725
726lemma lookup_prepare_trie_for_insertion_hit:
727 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
728  lookup … b (prepare_trie_for_insertion … b v) a = v.
729 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
730qed.
731 
732lemma lookup_insert_hit:
733 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
734  lookup … b (insert … b v t) a = v.
735 #A #a #v #n #b elim b -b -n //
736 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
737  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
738  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
739qed.
740
741coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
742
743lemma lookup_prepare_trie_for_insertion_miss:
744 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
745  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
746 #A #a #v #n #c elim c
747  [ #b >(BitVector_O … b) normalize #abs @⊥ //
748  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
749    cases hd cases hd' normalize
750    [2,3: #_ cases tl' //
751    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
752qed.
753 
754lemma lookup_insert_miss:
755 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
756  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
757 #A #a #v #n #c elim c -c -n
758  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
759  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
760    #t cases(BitVectorTrie_Sn … t)
761    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
762     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
763    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
764     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
765     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
766qed.
767
768definition load_code_memory_aux ≝
769 fold_left_i_aux … (
770   λi, mem, v.
771     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
772
773axiom split_elim:
774 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
775  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
776
777axiom half_add_SO:
778 ∀pc.
779 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
780
781(*
782axiom not_eqvb_S:
783 ∀pc.
784 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
785
786axiom not_eqvb_SS:
787 ∀pc.
788 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
789 
790axiom bitvector_elim_complete:
791 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
792
793lemma bitvector_elim_complete':
794 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
795 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
796 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
797qed.
798*)
799
800
801
802
803(*
804lemma andb_elim':
805 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
806 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
807qed.
808*)
809
810let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
811                       (encoding: list Byte) on encoding: Prop ≝
812  match encoding with
813  [ nil ⇒ final_pc = pc
814  | cons hd tl ⇒
815    let 〈new_pc, byte〉 ≝ next code_memory pc in
816      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
817  ].
818
819lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
820 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
821  let intermediate_pc ≝ pc + length … l1 in
822   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
823    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
824 #code_memory #final_pc #l1 elim l1
825  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
826  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
827    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
828qed.
829
830axiom  eq_bv_refl: ∀n,v. eq_bv n v v = true.
831
832axiom bitvector_3_elim_prop:
833 ∀P: BitVector 3 → Prop.
834  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
835  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
836  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
837
838axiom fetch_assembly:
839  ∀pc,i,code_memory,assembled.
840    assembled = assembly1 i →
841      let len ≝ length … assembled in
842      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
843      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
844      let 〈instr_pc, ticks〉 ≝ fetched in
845      let 〈instr,pc'〉 ≝ instr_pc in
846       (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
847(* #pc #i #code_memory #assembled cases i [8: *]
848 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
849 [47,48,49:
850 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
851  [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,
852   59,60,63,64,65,66,67: #ARG]]
853 [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,
854  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
855  [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,
856   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,
857   68,69,70,71: #ARG2]]
858 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
859 normalize in ⊢ (???% → ?)
860 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
861  normalize in ⊢ (???% → ?)]
862 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
863 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
864 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
865 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
866 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
867 [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,
868  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,
869  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
870 whd >eq_instruction_refl >H4 @eq_bv_refl
871qed. *)
872
873let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
874 match expected with
875  [ nil ⇒ eq_bv … pc final_pc = true
876  | cons i tl ⇒
877     let fetched ≝ fetch code_memory pc in
878     let 〈instr_pc, ticks〉 ≝ fetched in
879     let 〈instr,pc'〉 ≝ instr_pc in
880      eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl].
881
882lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
883 #A #a #b #EQ destruct //
884qed.
885
886lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
887 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
888qed.
889
890axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
891
892lemma fetch_assembly_pseudo:
893 ∀program,ppc,lookup_labels,lookup_datalabels.
894  ∀pi,code_memory,len,assembled,instructions,pc.
895   let expansion ≝ jump_expansion_policy program ppc in
896   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
897    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
898     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
899      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
900 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
901 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
902 >EQ2a >EQ2b -EQ2a EQ2b;
903  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
904  generalize in match pc elim instructions
905  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
906  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
907    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
908    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
909    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
910    >(eq_bv_to_eq … K2) @IH @H2 ]
911qed.
912
913
914(* This establishes the correspondence between pseudo program counters and
915   program counters. It is at the heart of the proof. *)
916(*CSC: code taken from build_maps *)
917definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
918 λinstr_list.
919  foldl ??
920    (λt. λi.
921       match t with
922       [ None ⇒ None ?
923       | Some ppc_pc_map ⇒
924         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
925         let 〈program_counter, sigma_map〉 ≝ pc_map in
926         let 〈label, i〉 ≝ i in
927          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
928           [ None ⇒ None ?
929           | Some pc_ignore ⇒
930              let 〈pc,ignore〉 ≝ pc_ignore in
931              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
932       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
933       
934definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
935 λinstr_list.
936  match sigma0 instr_list with
937   [ None ⇒ None …
938   | Some result ⇒
939      let 〈ppc,pc_sigma_map〉 ≝ result in
940       Some … pc_sigma_map ].
941
942definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
943 λinstr_list.
944  match sigma0 instr_list with
945  [ None ⇒ None ?
946  | Some result ⇒
947    let 〈ppc,pc_sigma_map〉 ≝ result in
948    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
949      if gtb pc (2^16) then
950        None ?
951      else
952        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
953
954axiom policy_ok: ∀p. sigma_safe p ≠ None ….
955
956definition sigma: pseudo_assembly_program → Word → Word ≝
957 λp.
958  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
959   [ None ⇒ λabs. ⊥
960   | Some r ⇒ λ_.r] (policy_ok p).
961 cases abs //
962qed.
963
964lemma length_append:
965 ∀A.∀l1,l2:list A.
966  |l1 @ l2| = |l1| + |l2|.
967 #A #l1 elim l1
968  [ //
969  | #hd #tl #IH #l2 normalize <IH //]
970qed.
971
972let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
973 match l with
974  [ nil ⇒ true
975  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
976
977lemma does_not_occur_None:
978 ∀id,i,list_instr.
979  does_not_occur id (list_instr@[〈None …,i〉]) =
980  does_not_occur id list_instr.
981 #id #i #list_instr elim list_instr
982  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
983qed.
984
985let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
986 match l with
987  [ nil ⇒ false
988  | cons hd tl ⇒
989     if instruction_matches_identifier id hd then
990      does_not_occur id tl
991     else
992      occurs_exactly_once id tl ].
993
994lemma occurs_exactly_once_None:
995 ∀id,i,list_instr.
996  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
997  occurs_exactly_once id list_instr.
998 #id #i #list_instr elim list_instr
999  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
1000qed.
1001
1002lemma index_of_internal_None: ∀i,id,instr_list,n.
1003 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1004  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1005   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
1006 #i #id #instr_list elim instr_list
1007  [ #n #abs whd in abs; cases abs
1008  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
1009    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
1010    [ #H %
1011    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
1012      [ #_ % | #abs cases abs ]]]
1013qed.
1014
1015lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1016 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1017  address_of_word_labels_code_mem instr_list id =
1018  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1019 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1020 >(index_of_internal_None … H) %
1021qed.
1022
1023axiom tech_pc_sigma0_append:
1024 ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
1025  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
1026   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
1027    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
1028
1029axiom tech_pc_sigma0_append_None:
1030 ∀preamble,instr_list,prefix,i,pc,costs.
1031  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
1032   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
1033    → False.
1034
1035(*
1036definition build_maps' ≝
1037  λpseudo_program.
1038  let 〈preamble,instr_list〉 ≝ pseudo_program in
1039  let result ≝
1040   foldl_strong
1041    (option Identifier × pseudo_instruction)
1042    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1043      let pre' ≝ 〈preamble,pre〉 in
1044      let 〈labels,pc_costs〉 ≝ res in
1045       tech_pc_sigma0 pre' = Some … pc_costs ∧
1046       ∀id. occurs_exactly_once id pre →
1047        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
1048    instr_list
1049    (λprefix,i,tl,prf,t.
1050      let 〈labels, pc_costs〉 ≝ t in
1051      let 〈program_counter, costs〉 ≝ pc_costs in
1052       let 〈label, i'〉 ≝ i in
1053       let labels ≝
1054         match label with
1055         [ None ⇒ labels
1056         | Some label ⇒
1057           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1058             insert ? ? label program_counter_bv labels
1059         ]
1060       in
1061         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
1062         [ None ⇒
1063            let dummy ≝ 〈labels,pc_costs〉 in
1064             dummy
1065         | Some construct ⇒ 〈labels, construct〉
1066         ]
1067    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
1068  in
1069   let 〈labels, pc_costs〉 ≝ result in
1070   let 〈pc, costs〉 ≝ pc_costs in
1071    〈labels, costs〉.
1072 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
1073 | whd cases construct in p3 #PC #CODE #JMEQ %
1074    [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
1075 | (* dummy case *) @⊥
1076   @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
1077 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
1078     >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
1079 whd in ⊢ (??(????%?)?) -labels1;
1080 cases label in Hid
1081  [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
1082     [ >(address_of_word_labels_code_mem_None … Hid)
1083       (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
1084     | whd in Hid >occurs_exactly_once_None in Hid // ]
1085  | -label #label #Hid whd in ⊢ (??(????%?)?)
1086   
1087  ]
1088qed.
1089
1090lemma build_maps_ok:
1091 ∀p:pseudo_assembly_program.
1092  let 〈labels,costs〉 ≝ build_maps' p in
1093   ∀pc.
1094    (nat_of_bitvector … pc) < length … (\snd p) →
1095     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
1096 #p cases p #preamble #instr_list
1097  elim instr_list
1098   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
1099   | #hd #tl #IH
1100    whd in ⊢ (match % with [ _ ⇒ ?])
1101   ]
1102qed.
1103*)
1104
1105axiom assembly_ok:
1106 ∀program,assembled,costs,labels,datalabels.
1107  Some … 〈labels,datalabels〉 = build_maps program →
1108  Some … 〈assembled,costs〉 = assembly program →
1109  let code_memory ≝ load_code_memory assembled in
1110  let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
1111  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1112   ∀ppc,len,assembledi.
1113    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1114     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
1115      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
1116       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
1117
1118lemma rev_preserves_length:
1119 ∀A.∀l. length … (rev A l) = length … l.
1120  #A #l elim l
1121   [ %
1122   | #hd #tl #IH normalize >length_append normalize /2/ ]
1123qed.
1124
1125lemma rev_append:
1126 ∀A.∀l1,l2.
1127  rev A (l1@l2) = rev A l2 @ rev A l1.
1128 #A #l1 elim l1 normalize //
1129qed.
1130 
1131lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
1132 #A #l elim l
1133  [ //
1134  | #hd #tl #IH normalize >rev_append normalize // ]
1135qed.
1136
1137lemma split_len_Sn:
1138 ∀A:Type[0].∀l:list A.∀len.
1139  length … l = S len →
1140   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
1141 #A #l elim l
1142  [ normalize #len #abs destruct
1143  | #hd #tl #IH #len
1144    generalize in match (rev_rev … tl)
1145    cases (rev A tl) in ⊢ (??%? → ?)
1146     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
1147     | #a #l' #H <H normalize #EQ
1148      %[@(hd::rev … l')] %[@a] % //
1149      >length_append in EQ #EQ normalize in EQ; normalize;
1150      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
1151qed.
1152
1153lemma list_elim_rev:
1154 ∀A:Type[0].∀P:list A → Type[0].
1155  P [ ] → (∀l,a. P l → P (l@[a])) →
1156   ∀l. P l.
1157 #A #P #H1 #H2 #l
1158 generalize in match (refl … (length … l))
1159 generalize in ⊢ (???% → ?) #n generalize in match l
1160 elim n
1161  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
1162  | #m #IH #L #EQ
1163    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
1164qed.
1165
1166axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
1167axiom prefix_of_append:
1168 ∀A:Type[0].∀l,l1,l2:list A.
1169  is_prefix … l l1 → is_prefix … l (l1@l2).
1170axiom prefix_reflexive: ∀A,l. is_prefix A l l.
1171axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
1172
1173record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
1174
1175definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
1176 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
1177
1178definition app ≝
1179 λA:Type[0].λl1:Propify (list A).λl2:list A.
1180  match l1 with
1181   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
1182
1183lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
1184 #A * /3/
1185qed.
1186
1187lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
1188 #A * #l1 normalize //
1189qed.
1190
1191let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
1192 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
1193 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
1194 B (app … prefix l) ≝
1195  match l with
1196  [ nil ⇒ ? (* b *)
1197  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1198  ].
1199 [ applyS b
1200 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
1201qed.
1202
1203(*
1204let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
1205 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
1206  match l with
1207  [ nil ⇒ ? (* b *)
1208  | cons hd tl ⇒
1209     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1210  ].
1211 [ applyS b
1212 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
1213qed.
1214*)
1215
1216definition foldll:
1217 ∀A:Type[0].∀B: Propify (list A) → Type[0].
1218  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
1219   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
1220 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1221
1222axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
1223axiom pprefix_of_append:
1224 ∀A:Type[0].∀l,l1,l2.
1225  is_pprefix A l l1 → is_pprefix A l (l1@l2).
1226axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
1227axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
1228
1229
1230axiom foldll':
1231 ∀A:Type[0].∀l: list A.
1232  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
1233  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
1234   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
1235 #A #l #B
1236 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
1237 
1238 
1239  #H #acc
1240 @foldll
1241  [
1242  |
1243  ]
1244 
1245 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1246
1247
1248(*
1249record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
1250 { subset_wit:> A;
1251   subset_proof: P subset_wit
1252 }.
1253*)
1254
1255definition build_maps' ≝
1256  λpseudo_program.
1257  let 〈preamble,instr_list〉 ≝ pseudo_program in
1258  let result ≝
1259   foldll
1260    (option Identifier × pseudo_instruction)
1261    (λprefix.
1262      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1263       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
1264    (λprefix,t,i.
1265      let 〈labels, pc_costs〉 ≝ t in
1266      let 〈program_counter, costs〉 ≝ pc_costs in
1267       let 〈label, i'〉 ≝ i in
1268       let labels ≝
1269         match label with
1270         [ None ⇒ labels
1271         | Some label ⇒
1272           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1273             insert ? ? label program_counter_bv labels
1274         ]
1275       in
1276         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1277         [ None ⇒
1278            let dummy ≝ 〈labels,pc_costs〉 in
1279              dummy
1280         | Some construct ⇒ 〈labels, construct〉
1281         ]
1282    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
1283  in
1284   let 〈labels, pc_costs〉 ≝ result in
1285   let 〈pc, costs〉 ≝ pc_costs in
1286    〈labels, costs〉.
1287 [
1288 | @⊥
1289 | normalize % //
1290 ]
1291qed.
1292
1293definition build_maps' ≝
1294  λpseudo_program.
1295  let 〈preamble,instr_list〉 ≝ pseudo_program in
1296  let result ≝
1297   foldl
1298    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1299          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1300           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
1301    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1302          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1303           is_prefix ? instr_list_prefix' instr_list →
1304           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
1305    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1306          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1307           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
1308     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1309          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1310           is_prefix ? instr_list_prefix' instr_list →
1311           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
1312      let 〈labels, pc_costs〉 ≝ t in
1313      let 〈program_counter, costs〉 ≝ pc_costs in
1314       let 〈label, i'〉 ≝ i in
1315       let labels ≝
1316         match label with
1317         [ None ⇒ labels
1318         | Some label ⇒
1319           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1320             insert ? ? label program_counter_bv labels
1321         ]
1322       in
1323         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1324         [ None ⇒
1325            let dummy ≝ 〈labels,pc_costs〉 in
1326              dummy
1327         | Some construct ⇒ 〈labels, construct〉
1328         ]
1329    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
1330  in
1331   let 〈labels, pc_costs〉 ≝ result in
1332   let 〈pc, costs〉 ≝ pc_costs in
1333    〈labels, costs〉.
1334 [4: @(list_elim_rev ?
1335       (λinstr_list. list (
1336        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1337          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1338           is_prefix ? instr_list_prefix' instr_list →
1339           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
1340       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
1341      [ @[ ]
1342      | #l' #a #limage %2
1343        [ %[@a] #PREFIX #PREFIX_OK
1344        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
1345             THE INDUCTION HYPOTHESIS INSTEAD *)
1346          elim limage
1347           [ %1
1348           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
1349             @K1 @(prefix_of_append ???? K3)
1350           ] 
1351        ]
1352       
1353       
1354     
1355 
1356  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
1357     % [@ (LIST_PREFIX @ [i])] %
1358      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
1359      | (* DOABLE IN PRINCIPLE *)
1360      ]
1361 | (* assert false case *)
1362 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
1363 |   
1364
1365definition assembly_specification:
1366  ∀assembly_program: pseudo_assembly_program.
1367  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1368  λpseudo_assembly_program.
1369  λcode_mem.
1370    ∀pc: Word.
1371      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1372      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1373      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1374      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1375      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1376       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1377      match pre_assembled with
1378       [ None ⇒ True
1379       | Some pc_code ⇒
1380          let 〈new_pc,code〉 ≝ pc_code in
1381           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1382
1383axiom assembly_meets_specification:
1384  ∀pseudo_assembly_program.
1385    match assembly pseudo_assembly_program with
1386    [ None ⇒ True
1387    | Some code_mem_cost ⇒
1388      let 〈code_mem, cost〉 ≝ code_mem_cost in
1389        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1390    ].
1391(*
1392  # PROGRAM
1393  [ cases PROGRAM
1394    # PREAMBLE
1395    # INSTR_LIST
1396    elim INSTR_LIST
1397    [ whd
1398      whd in ⊢ (∀_. %)
1399      # PC
1400      whd
1401    | # INSTR
1402      # INSTR_LIST_TL
1403      # H
1404      whd
1405      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1406    ]
1407  | cases not_implemented
1408  ] *)
1409
1410definition status_of_pseudo_status: PseudoStatus → option Status ≝
1411 λps.
1412  let pap ≝ code_memory … ps in
1413   match assembly pap with
1414    [ None ⇒ None …
1415    | Some p ⇒
1416       let cm ≝ load_code_memory (\fst p) in
1417       let pc ≝ sigma' pap (program_counter ? ps) in
1418        Some …
1419         (mk_PreStatus (BitVectorTrie Byte 16)
1420           cm
1421           (low_internal_ram … ps)
1422           (high_internal_ram … ps)
1423           (external_ram … ps)
1424           pc
1425           (special_function_registers_8051 … ps)
1426           (special_function_registers_8052 … ps)
1427           (p1_latch … ps)
1428           (p3_latch … ps)
1429           (clock … ps)) ].
1430
1431definition write_at_stack_pointer':
1432 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1433  λM: Type[0].
1434  λs: PreStatus M.
1435  λv: Byte.
1436    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1437    let bit_zero ≝ get_index_v… nu O ? in
1438    let bit_1 ≝ get_index_v… nu 1 ? in
1439    let bit_2 ≝ get_index_v… nu 2 ? in
1440    let bit_3 ≝ get_index_v… nu 3 ? in
1441      if bit_zero then
1442        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1443                              v (low_internal_ram ? s) in
1444          set_low_internal_ram ? s memory
1445      else
1446        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1447                              v (high_internal_ram ? s) in
1448          set_high_internal_ram ? s memory.
1449  [ cases l0 %
1450  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1451qed.
1452
1453definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1454 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1455
1456  λticks_of.
1457  λs.
1458  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1459  let ticks ≝ ticks_of (program_counter ? s) in
1460  let s ≝ set_clock ? s (clock ? s + ticks) in
1461  let s ≝ set_program_counter ? s pc in
1462    match instr with
1463    [ Instruction instr ⇒
1464       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1465    | Comment cmt ⇒ s
1466    | Cost cst ⇒ s
1467    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1468    | Call call ⇒
1469      let a ≝ address_of_word_labels s call in
1470      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1471      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1472      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1473      let s ≝ write_at_stack_pointer' ? s pc_bl in
1474      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1475      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1476      let s ≝ write_at_stack_pointer' ? s pc_bu in
1477        set_program_counter ? s a
1478    | Mov dptr ident ⇒
1479       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1480    ].
1481 [
1482 |2,3,4: %
1483 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1484 |
1485 | %
1486 ]
1487 cases not_implemented
1488qed.
1489
1490(*
1491lemma execute_code_memory_unchanged:
1492 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1493 #ticks #ps whd in ⊢ (??? (??%))
1494 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1495  (program_counter pseudo_assembly_program ps)) #instr #pc
1496 whd in ⊢ (??? (??%)) cases instr
1497  [ #pre cases pre
1498     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1499       cases (split ????) #z1 #z2 %
1500     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1501       cases (split ????) #z1 #z2 %
1502     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1503       cases (split ????) #z1 #z2 %
1504     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1505       [ #x1 whd in ⊢ (??? (??%))
1506     | *: cases not_implemented
1507     ]
1508  | #comment %
1509  | #cost %
1510  | #label %
1511  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1512    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1513    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1514    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1515    (* CSC: ??? *)
1516  | #dptr #label (* CSC: ??? *)
1517  ]
1518  cases not_implemented
1519qed.
1520*)
1521
1522lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1523 ∀ps,ps': PseudoStatus.
1524  code_memory … ps = code_memory … ps' →
1525   match status_of_pseudo_status ps with
1526    [ None ⇒ status_of_pseudo_status ps' = None …
1527    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
1528    ].
1529 #ps #ps' #H whd in ⊢ (mat
1530 ch % with [ _ ⇒ ? | _ ⇒ ? ])
1531 generalize in match (refl … (assembly (code_memory … ps)))
1532 cases (assembly ?) in ⊢ (???% → %)
1533  [ #K whd whd in ⊢ (??%?) <H >K %
1534  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1535qed.*)
1536
1537let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
1538  match encoding with
1539  [ nil ⇒ True
1540  | cons hd tl ⇒
1541    let 〈new_pc, byte〉 ≝ next code_memory pc in
1542      hd = byte ∧ encoding_check' code_memory new_pc tl
1543  ].
1544 
1545lemma main_thm:
1546 ∀ticks_of.
1547 ∀ps: PseudoStatus.
1548  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
1549  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
1550  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
1551  let s' ≝ execute_1 s in
1552   s = s'']].
1553 #ticks_of #ps
1554 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1555 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
1556 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1557 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
1558 
1559 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.