source: src/ASM/AssemblyProof.ma @ 863

Last change on this file since 863 was 863, checked in by sacerdot, 10 years ago

Yet another fix to the statement.

File size: 31.2 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
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_associativity_of_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       
118axiom vector_cons_append:
119  ∀A: Type[0].
120  ∀n: nat.
121  ∀a: A.
122  ∀v: Vector A n.
123    a ::: v = [[ a ]] @@ v.
124
125lemma super_rewrite2:
126 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
127  ∀P: ∀m. Vector A m → Prop.
128   n=m → v1 ≃ v2 → P n v1 → P m v2.
129 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
130qed.
131
132lemma mem_middle_vector:
133  ∀A: Type[0].
134  ∀m, o: nat.
135  ∀eq: A → A → bool.
136  ∀reflex: ∀a. eq a a = true.
137  ∀p: Vector A m.
138  ∀a: A.
139  ∀r: Vector A o.
140    mem A eq ? (p@@(a:::r)) a = true.
141  # A # M # O # EQ # REFLEX # P # A
142  elim P
143  [ normalize
144    > (REFLEX A)
145    normalize
146    # H
147    %
148  | # NN # AA # PP # IH
149    normalize
150    cases (EQ A AA) //
151     @ IH
152  ]
153qed.
154
155lemma mem_monotonic_wrt_append:
156  ∀A: Type[0].
157  ∀m, o: nat.
158  ∀eq: A → A → bool.
159  ∀reflex: ∀a. eq a a = true.
160  ∀p: Vector A m.
161  ∀a: A.
162  ∀r: Vector A o.
163    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
164  # A # M # O # EQ # REFLEX # P # A
165  elim P
166  [ #R #H @H
167  | #NN #AA # PP # IH #R #H
168    normalize
169    cases (EQ A AA)
170    [ normalize %
171    | @ IH @ H
172    ]
173  ]
174qed.
175
176lemma subvector_hd_tl:
177  ∀A: Type[0].
178  ∀o, n: nat.
179  ∀eq: A → A → bool.
180  ∀refl: ∀a. eq a a = true.
181  ∀h: Vector A o.
182  ∀v: Vector A n.
183  ∀m: nat.
184  ∀q: Vector A m.
185    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
186  # A # O # N # EQ # REFLEX # H # V
187  elim V
188  [ normalize
189    # M # V %
190  | # NN # AA # VV # IH # MM # QQ
191    change with (bool_to_Prop (andb ??))
192    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
193    [
194    | # HH > HH
195      > (vector_cons_append ? ? AA VV)
196      change with (bool_to_Prop (subvector_with ??????))
197      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
198        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
199        ?
200        (vector_associativity_of_append A ? ? ? QQ [[AA]] VV))
201      [ >associative_plus //
202      | @IH ]
203    ]
204    @(mem_monotonic_wrt_append)
205    [ @ REFLEX
206    | @(mem_monotonic_wrt_append)
207      [ @ REFLEX
208      | normalize
209        > REFLEX
210        normalize
211        %
212      ]
213    ]
214qed.
215(*
216lemma subvector_hd_tl:
217  ∀A: Type[0].
218  ∀n: nat.
219  ∀h: A.
220  ∀eq: A → A → bool.
221  ∀v: Vector A n.
222  ∀m: nat.
223  ∀q: Vector A m.
224    bool_to_Prop (subvector_with A ? ? eq v (h ::: q @@ v)).
225  # A
226  # N
227  # H
228  # EQ
229  # V
230  elim V
231  [ normalize
232    # M
233    # Q
234    %
235  | # NN
236    # AA
237    # VV
238    # IH
239    # MM
240    # QQ
241    whd
242    whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
243    change in ⊢ (match (match ? with [_ ⇒ % | _ ⇒ ?]) with [_ ⇒ ? | _ ⇒ ?])
244     with (subvector_with ??????)
245    change in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]) with (andb ??)
246    change with (bool_to_Prop ?);
247    cut ((mem A EQ (S MM+S NN) (H:::QQ@@AA:::VV) AA) = true)
248    [
249    | # H
250      > H
251      applyS (IH ? (QQ@@[[AA]]))
252    ]
253    generalize in match (IH ? (QQ@@[[AA]]))
254    whd in ⊢ (% → ?)
255  ]
256  *)
257
258(*
259let rec list_addressing_mode_tags_elim
260  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
261  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
262   (l → bool) → bool ] with
263  [ VEmpty      ⇒  true 
264  | VCons len hd tl ⇒ λP.
265    let process_hd ≝
266      match hd return λhd. ∀P: hd:::tl → bool. bool with
267      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
268      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
269      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
270      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
271      | acc_a ⇒ λP.P ACC_A
272      | acc_b ⇒ λP.P ACC_B
273      | dptr ⇒ λP.P DPTR
274      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
275      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
276      | acc_dptr ⇒ λP.P ACC_DPTR
277      | acc_pc ⇒ λP.P ACC_PC
278      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
279      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
280      | carry ⇒ λP.P CARRY
281      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
282      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
283      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
284      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
285      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
286      ]
287    in
288      andb (process_hd P)
289       (match len return λlen. Vector addressing_mode_tag len → bool with
290         [ O ⇒ λ_.true
291         | S y ⇒ λtl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl)
292  ].
293  [1: @ (execute_1_technical ? ? tl)
294      [ //
295      |
296      ]
297  ].
298
299definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
300 λP.
301   P (ADD … ACC_A
302   P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
303 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
304qed.
305 %
306qed.
307 
308
309definition instruction_elim: ∀P: instruction → bool. bool.
310 
311 
312lemma instruction_elim_correct:
313  ∀i: instruction.
314  ∀P: instruction → bool.
315    instruction_elim P = true → ∀j. P j = true.
316 
317lemma test:
318  ∀i: instruction.
319  ∃pc.
320  let assembled ≝ assembly1 i in
321  let code_memory ≝ load_code_memory assembled in
322  let fetched ≝ fetch code_memory pc in
323  let 〈instr_pc, ticks〉 ≝ fetched in
324    \fst instr_pc = i.
325  # INSTR
326  @ (ex_intro ?)
327  [ @ (zero 16)
328  | @ (instruction_elim INSTR)
329  ].
330*)
331 
332(* This establishes the correspondence between pseudo program counters and
333   program counters. It is at the heart of the proof. *)
334(*CSC: code taken from build_maps *)
335definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
336 λinstr_list.
337  foldl ??
338    (λt. λi.
339       match t with
340       [ None ⇒ None ?
341       | Some ppc_pc_map ⇒
342         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
343         let 〈program_counter, sigma_map〉 ≝ pc_map in
344         let 〈label, i〉 ≝ i in
345          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
346           [ None ⇒ None ?
347           | Some pc_ignore ⇒
348              let 〈pc,ignore〉 ≝ pc_ignore in
349              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
350       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
351       
352definition tech_pc_sigma0: pseudo_assembly_program → option nat ≝
353 λinstr_list.
354  match sigma0 instr_list with
355   [ None ⇒ None …
356   | Some result ⇒
357      let 〈ppc,pc_sigma_map〉 ≝ result in
358      let 〈pc, sigma_map〉 ≝ pc_sigma_map in
359       Some … pc ].
360
361definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
362 λinstr_list.
363  match sigma0 instr_list with
364  [ None ⇒ None ?
365  | Some result ⇒
366    let 〈ppc,pc_sigma_map〉 ≝ result in
367    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
368      if gtb pc (2^16) then
369        None ?
370      else
371        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
372
373axiom policy_ok: ∀p. sigma_safe p ≠ None ….
374
375definition sigma: pseudo_assembly_program → Word → Word ≝
376 λp.
377  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
378   [ None ⇒ λabs. ⊥
379   | Some r ⇒ λ_.r] (policy_ok p).
380 cases abs //
381qed.
382
383lemma length_append:
384 ∀A.∀l1,l2:list A.
385  |l1 @ l2| = |l1| + |l2|.
386 #A #l1 elim l1
387  [ //
388  | #hd #tl #IH #l2 normalize <IH //]
389qed.
390
391let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
392 match l with
393  [ nil ⇒ true
394  | cons hd tl ⇒ notb (address_of_word_labels_internal id hd) ∧ does_not_occur id tl].
395
396lemma does_not_occur_None:
397 ∀id,i,list_instr.
398  does_not_occur id (list_instr@[〈None …,i〉]) =
399  does_not_occur id list_instr.
400 #id #i #list_instr elim list_instr
401  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
402qed.
403
404let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
405 match l with
406  [ nil ⇒ false
407  | cons hd tl ⇒
408     if address_of_word_labels_internal id hd then
409      does_not_occur id tl
410     else
411      occurs_exactly_once id tl ].
412
413lemma occurs_exactly_once_None:
414 ∀id,i,list_instr.
415  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
416  occurs_exactly_once id list_instr.
417 #id #i #list_instr elim list_instr
418  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
419qed.
420
421coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
422
423lemma index_of_internal_None: ∀i,id,instr_list,n.
424 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
425  index_of_internal ? (address_of_word_labels_internal id) instr_list n =
426   index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
427 #i #id #instr_list elim instr_list
428  [ #n #abs whd in abs; cases abs
429  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
430    cases (address_of_word_labels_internal id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
431    [ #H %
432    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
433      [ #_ % | #abs cases abs ]]]
434qed.
435
436lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
437 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
438  address_of_word_labels_code_mem instr_list id =
439  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
440 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
441 >(index_of_internal_None … H) %
442qed.
443
444definition build_maps' ≝
445  λpseudo_program.
446  let 〈preamble,instr_list〉 ≝ pseudo_program in
447  let result ≝
448   foldl_strong
449    (option Identifier × pseudo_instruction)
450    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
451      let pre' ≝ 〈preamble,pre〉 in
452      let 〈labels,pc_costs〉 ≝ res in
453      let 〈program_counter,costs〉 ≝ pc_costs in
454       tech_pc_sigma0 pre' = Some … program_counter ∧
455       ∀id. occurs_exactly_once id pre →
456        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
457    instr_list
458    (λprefix,i,tl,prf,t.
459      let 〈labels, pc_costs〉 ≝ t in
460      let 〈program_counter, costs〉 ≝ pc_costs in
461       let 〈label, i'〉 ≝ i in
462       let labels ≝
463         match label with
464         [ None ⇒ labels
465         | Some label ⇒
466           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
467             insert ? ? label program_counter_bv labels
468         ]
469       in
470         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
471         [ None ⇒
472            let dummy ≝ 〈labels,pc_costs〉 in
473             dummy
474         | Some construct ⇒ 〈labels, construct〉
475         ]
476    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
477  in
478   let 〈labels, pc_costs〉 ≝ result in
479   let 〈pc, costs〉 ≝ pc_costs in
480    〈labels, costs〉.
481 [ whd cases construct in p3 #PC #CODE #JMEQ whd %
482    [
483    | #id #Hid
484      generalize in match (sig2 … t) whd in ⊢ (% → ?)
485      >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) * #IH0 #IH1
486      whd in ⊢ (??(????%?)?) -labels1;
487      cases label in Hid
488       [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
489          [ >(address_of_word_labels_code_mem_None … Hid)
490            (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
491          | whd in Hid >occurs_exactly_once_None in Hid // ]
492       | -label #label #Hid whd in ⊢ (??(????%?)?)
493     
494       ]]
495 | (* dummy case *)
496 | whd % // #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
497qed.
498
499(*
500(*
501notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
502 with precedence 10
503for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
504*)
505
506lemma build_maps_ok:
507 ∀p:pseudo_assembly_program.
508  let 〈labels,costs〉 ≝ build_maps' p in
509   ∀pc.
510    (nat_of_bitvector … pc) < length … (\snd p) →
511     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
512 #p cases p #preamble #instr_list
513  elim instr_list
514   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
515   | #hd #tl #IH
516    whd in ⊢ (match % with [ _ ⇒ ?])
517   ]
518qed.
519*)
520
521(*
522lemma list_elim_rev:
523 ∀A:Type[0].∀P:list A → Prop.
524  P [ ] → (∀n,l. length l = n → P l → 
525  P [ ] → (∀l,a. P l → P (l@[a])) →
526   ∀l. P l.
527 #A #P
528qed.*)
529
530lemma rev_preserves_length:
531 ∀A.∀l. length … (rev A l) = length … l.
532  #A #l elim l
533   [ %
534   | #hd #tl #IH normalize >length_append normalize /2/ ]
535qed.
536
537lemma rev_append:
538 ∀A.∀l1,l2.
539  rev A (l1@l2) = rev A l2 @ rev A l1.
540 #A #l1 elim l1 normalize //
541qed.
542 
543lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
544 #A #l elim l
545  [ //
546  | #hd #tl #IH normalize >rev_append normalize // ]
547qed.
548
549lemma split_len_Sn:
550 ∀A:Type[0].∀l:list A.∀len.
551  length … l = S len →
552   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
553 #A #l elim l
554  [ normalize #len #abs destruct
555  | #hd #tl #IH #len
556    generalize in match (rev_rev … tl)
557    cases (rev A tl) in ⊢ (??%? → ?)
558     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
559     | #a #l' #H <H normalize #EQ
560      %[@(hd::rev … l')] %[@a] % //
561      >length_append in EQ #EQ normalize in EQ; normalize;
562      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
563qed.
564
565lemma list_elim_rev:
566 ∀A:Type[0].∀P:list A → Type[0].
567  P [ ] → (∀l,a. P l → P (l@[a])) →
568   ∀l. P l.
569 #A #P #H1 #H2 #l
570 generalize in match (refl … (length … l))
571 generalize in ⊢ (???% → ?) #n generalize in match l
572 elim n
573  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
574  | #m #IH #L #EQ
575    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
576qed.
577
578axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
579axiom prefix_of_append:
580 ∀A:Type[0].∀l,l1,l2:list A.
581  is_prefix … l l1 → is_prefix … l (l1@l2).
582axiom prefix_reflexive: ∀A,l. is_prefix A l l.
583axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
584
585record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
586
587definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
588 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
589
590definition app ≝
591 λA:Type[0].λl1:Propify (list A).λl2:list A.
592  match l1 with
593   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
594
595lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
596 #A * /3/
597qed.
598
599lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
600 #A * #l1 normalize //
601qed.
602
603let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
604 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
605 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
606 B (app … prefix l) ≝
607  match l with
608  [ nil ⇒ ? (* b *)
609  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
610  ].
611 [ applyS b
612 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
613qed.
614
615(*
616let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
617 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
618  match l with
619  [ nil ⇒ ? (* b *)
620  | cons hd tl ⇒
621     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
622  ].
623 [ applyS b
624 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
625qed.
626*)
627
628definition foldll:
629 ∀A:Type[0].∀B: Propify (list A) → Type[0].
630  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
631   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
632 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
633
634axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
635axiom pprefix_of_append:
636 ∀A:Type[0].∀l,l1,l2.
637  is_pprefix A l l1 → is_pprefix A l (l1@l2).
638axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
639axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
640
641
642axiom foldll':
643 ∀A:Type[0].∀l: list A.
644  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
645  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
646   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
647 #A #l #B
648 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
649 
650 
651  #H #acc
652 @foldll
653  [
654  |
655  ]
656 
657 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
658
659
660(*
661record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
662 { subset_wit:> A;
663   subset_proof: P subset_wit
664 }.
665*)
666
667definition build_maps' ≝
668  λpseudo_program.
669  let 〈preamble,instr_list〉 ≝ pseudo_program in
670  let result ≝
671   foldll
672    (option Identifier × pseudo_instruction)
673    (λprefix.
674      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
675       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
676    (λprefix,t,i.
677      let 〈labels, pc_costs〉 ≝ t in
678      let 〈program_counter, costs〉 ≝ pc_costs in
679       let 〈label, i'〉 ≝ i in
680       let labels ≝
681         match label with
682         [ None ⇒ labels
683         | Some label ⇒
684           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
685             insert ? ? label program_counter_bv labels
686         ]
687       in
688         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
689         [ None ⇒
690            let dummy ≝ 〈labels,pc_costs〉 in
691              dummy
692         | Some construct ⇒ 〈labels, construct〉
693         ]
694    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
695  in
696   let 〈labels, pc_costs〉 ≝ result in
697   let 〈pc, costs〉 ≝ pc_costs in
698    〈labels, costs〉.
699 [
700 | @⊥
701 | normalize % //
702 ]
703qed.
704
705definition build_maps' ≝
706  λpseudo_program.
707  let 〈preamble,instr_list〉 ≝ pseudo_program in
708  let result ≝
709   foldl
710    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
711          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
712           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
713    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
714          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
715           is_prefix ? instr_list_prefix' instr_list →
716           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
717    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
718          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
719           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
720     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
721          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
722           is_prefix ? instr_list_prefix' instr_list →
723           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
724      let 〈labels, pc_costs〉 ≝ t in
725      let 〈program_counter, costs〉 ≝ pc_costs in
726       let 〈label, i'〉 ≝ i in
727       let labels ≝
728         match label with
729         [ None ⇒ labels
730         | Some label ⇒
731           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
732             insert ? ? label program_counter_bv labels
733         ]
734       in
735         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
736         [ None ⇒
737            let dummy ≝ 〈labels,pc_costs〉 in
738              dummy
739         | Some construct ⇒ 〈labels, construct〉
740         ]
741    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
742  in
743   let 〈labels, pc_costs〉 ≝ result in
744   let 〈pc, costs〉 ≝ pc_costs in
745    〈labels, costs〉.
746 [4: @(list_elim_rev ?
747       (λinstr_list. list (
748        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
749          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
750           is_prefix ? instr_list_prefix' instr_list →
751           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
752       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
753      [ @[ ]
754      | #l' #a #limage %2
755        [ %[@a] #PREFIX #PREFIX_OK
756        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
757             THE INDUCTION HYPOTHESIS INSTEAD *)
758          elim limage
759           [ %1
760           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
761             @K1 @(prefix_of_append ???? K3)
762           ] 
763        ]
764       
765       
766     
767 
768  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
769     % [@ (LIST_PREFIX @ [i])] %
770      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
771      | (* DOABLE IN PRINCIPLE *)
772      ]
773 | (* assert false case *)
774 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
775 |   
776
777let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
778                       (encoding: list Byte) on encoding: Prop ≝
779  match encoding with
780  [ nil ⇒ final_pc = pc
781  | cons hd tl ⇒
782    let 〈new_pc, byte〉 ≝ next code_memory pc in
783      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
784  ].
785
786definition assembly_specification:
787  ∀assembly_program: pseudo_assembly_program.
788  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
789  λpseudo_assembly_program.
790  λcode_mem.
791    ∀pc: Word.
792      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
793      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
794      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
795      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
796      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
797       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
798      match pre_assembled with
799       [ None ⇒ True
800       | Some pc_code ⇒
801          let 〈new_pc,code〉 ≝ pc_code in
802           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
803
804axiom assembly_meets_specification:
805  ∀pseudo_assembly_program.
806    match assembly pseudo_assembly_program with
807    [ None ⇒ True
808    | Some code_mem_cost ⇒
809      let 〈code_mem, cost〉 ≝ code_mem_cost in
810        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
811    ].
812(*
813  # PROGRAM
814  [ cases PROGRAM
815    # PREAMBLE
816    # INSTR_LIST
817    elim INSTR_LIST
818    [ whd
819      whd in ⊢ (∀_. %)
820      # PC
821      whd
822    | # INSTR
823      # INSTR_LIST_TL
824      # H
825      whd
826      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
827    ]
828  | cases not_implemented
829  ] *)
830
831definition status_of_pseudo_status: PseudoStatus → option Status ≝
832 λps.
833  let pap ≝ code_memory … ps in
834   match assembly pap with
835    [ None ⇒ None …
836    | Some p ⇒
837       let cm ≝ load_code_memory (\fst p) in
838       let pc ≝ sigma' pap (program_counter ? ps) in
839        Some …
840         (mk_PreStatus (BitVectorTrie Byte 16)
841           cm
842           (low_internal_ram … ps)
843           (high_internal_ram … ps)
844           (external_ram … ps)
845           pc
846           (special_function_registers_8051 … ps)
847           (special_function_registers_8052 … ps)
848           (p1_latch … ps)
849           (p3_latch … ps)
850           (clock … ps)) ].
851
852definition write_at_stack_pointer':
853 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
854  λM: Type[0].
855  λs: PreStatus M.
856  λv: Byte.
857    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
858    let bit_zero ≝ get_index_v… nu O ? in
859    let bit_1 ≝ get_index_v… nu 1 ? in
860    let bit_2 ≝ get_index_v… nu 2 ? in
861    let bit_3 ≝ get_index_v… nu 3 ? in
862      if bit_zero then
863        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
864                              v (low_internal_ram ? s) in
865          set_low_internal_ram ? s memory
866      else
867        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
868                              v (high_internal_ram ? s) in
869          set_high_internal_ram ? s memory.
870  [ cases l0 %
871  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
872qed.
873
874definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
875 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
876
877  λticks_of.
878  λs.
879  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
880  let ticks ≝ ticks_of (program_counter ? s) in
881  let s ≝ set_clock ? s (clock ? s + ticks) in
882  let s ≝ set_program_counter ? s pc in
883    match instr with
884    [ Instruction instr ⇒
885       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
886    | Comment cmt ⇒ s
887    | Cost cst ⇒ s
888    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
889    | Call call ⇒
890      let a ≝ address_of_word_labels s call in
891      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
892      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
893      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
894      let s ≝ write_at_stack_pointer' ? s pc_bl in
895      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
896      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
897      let s ≝ write_at_stack_pointer' ? s pc_bu in
898        set_program_counter ? s a
899    | Mov dptr ident ⇒
900       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
901    ].
902 [
903 |2,3,4: %
904 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
905 |
906 | %
907 ]
908 cases not_implemented
909qed.
910
911(*
912lemma execute_code_memory_unchanged:
913 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
914 #ticks #ps whd in ⊢ (??? (??%))
915 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
916  (program_counter pseudo_assembly_program ps)) #instr #pc
917 whd in ⊢ (??? (??%)) cases instr
918  [ #pre cases pre
919     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
920       cases (split ????) #z1 #z2 %
921     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
922       cases (split ????) #z1 #z2 %
923     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
924       cases (split ????) #z1 #z2 %
925     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
926       [ #x1 whd in ⊢ (??? (??%))
927     | *: cases not_implemented
928     ]
929  | #comment %
930  | #cost %
931  | #label %
932  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
933    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
934    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
935    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
936    (* CSC: ??? *)
937  | #dptr #label (* CSC: ??? *)
938  ]
939  cases not_implemented
940qed.
941*)
942
943lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
944 ∀ps,ps': PseudoStatus.
945  code_memory … ps = code_memory … ps' →
946   match status_of_pseudo_status ps with
947    [ None ⇒ status_of_pseudo_status ps' = None …
948    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
949    ].
950 #ps #ps' #H whd in ⊢ (mat
951 ch % with [ _ ⇒ ? | _ ⇒ ? ])
952 generalize in match (refl … (assembly (code_memory … ps)))
953 cases (assembly ?) in ⊢ (???% → %)
954  [ #K whd whd in ⊢ (??%?) <H >K %
955  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
956qed.*)
957
958let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
959  match encoding with
960  [ nil ⇒ True
961  | cons hd tl ⇒
962    let 〈new_pc, byte〉 ≝ next code_memory pc in
963      hd = byte ∧ encoding_check' code_memory new_pc tl
964  ].
965
966(* prove later *)
967axiom test:
968  ∀pc: Word.
969  ∀code_memory: BitVectorTrie Byte 16.
970  ∀i: instruction.
971    let assembled ≝ assembly1 i in
972      encoding_check' code_memory pc assembled →
973        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
974        let 〈instr, pc〉 ≝ instr_pc in
975          instr = i.
976 
977lemma main_thm:
978 ∀ticks_of.
979 ∀ps: PseudoStatus.
980  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
981  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
982  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
983  let s' ≝ execute_1 s in
984   s = s'']].
985 #ticks_of #ps
986 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
987 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
988 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
989 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
990 
991 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.