# source:src/ASM/AssemblyProof.ma@892

Last change on this file since 892 was 892, checked in by sacerdot, 9 years ago

First fundamental lemma almost finished.

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