source:src/ASM/AssemblyProof.ma@861

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

Statement of the lemma fixed (again!)
Some preliminary work on additional lemmas.

File size: 29.8 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
391axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
392
393lemma index_of_internal_None: ∀i,id,instr_list,n.
394 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
395  index_of_internal ? (address_of_word_labels_internal id) instr_list n =
396   index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
397 #i #id #instr_list elim instr_list
398  [ #n #abs (* ASSURDO *)
399  | #hd #tl #IH #n #H whd in ⊢ (??%%) cases (address_of_word_labels_internal id hd)
400    whd in ⊢ (??%%)
401    [ %
402    | @IH
403    ]]
404qed.
405
406lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
407 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
408  address_of_word_labels_code_mem instr_list id =
409  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
410 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
411
412definition build_maps' ≝
413  λpseudo_program.
414  let 〈preamble,instr_list〉 ≝ pseudo_program in
415  let result ≝
416   foldl_strong
417    (option Identifier × pseudo_instruction)
418    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
419      let pre' ≝ 〈preamble,pre〉 in
420      let 〈labels,pc_costs〉 ≝ res in
421      let 〈ignore,costs〉 ≝ pc_costs in
422       ∀id. occurs_exactly_once id pre →
423        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
424    instr_list
425    (λprefix,i,tl,prf,t.
426      let 〈labels, pc_costs〉 ≝ t in
427      let 〈program_counter, costs〉 ≝ pc_costs in
428       let 〈label, i'〉 ≝ i in
429       let labels ≝
430         match label with
431         [ None ⇒ labels
432         | Some label ⇒
433           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
434             insert ? ? label program_counter_bv labels
435         ]
436       in
437         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
438         [ None ⇒
439            let dummy ≝ 〈labels,pc_costs〉 in
440             dummy
441         | Some construct ⇒ 〈labels, construct〉
442         ]
443    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
444  in
445   let 〈labels, pc_costs〉 ≝ result in
446   let 〈pc, costs〉 ≝ pc_costs in
447    〈labels, costs〉.
448 [ whd cases construct in p3 #PC #CODE #JMEQ whd #id #Hid
449   generalize in match (sig2 … t) whd in ⊢ (% → ?)
450   >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
451   whd in ⊢ (??(????%?)?) -labels1;
452   cases label in Hid
453    [ #Hid whd in ⊢ (??(????%?)?)
454      (* COMPLETARE *)
455      >IH1 -IH1
456       [
457       |
458       ]
459    | -label #label whd in ⊢ (??(????%?)?)
460
461    ]
462 | (* dummy case *)
463 | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
464qed.
465
466(*
467(*
468notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
469 with precedence 10
470for @{ match \$t with [ pair \${ident x} \${ident y} ⇒ \$s ] }.
471*)
472
473lemma build_maps_ok:
474 ∀p:pseudo_assembly_program.
475  let 〈labels,costs〉 ≝ build_maps' p in
476   ∀pc.
477    (nat_of_bitvector … pc) < length … (\snd p) →
478     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
479 #p cases p #preamble #instr_list
480  elim instr_list
481   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
482   | #hd #tl #IH
483    whd in ⊢ (match % with [ _ ⇒ ?])
484   ]
485qed.
486*)
487
488(*
489lemma list_elim_rev:
490 ∀A:Type[0].∀P:list A → Prop.
491  P [ ] → (∀n,l. length l = n → P l →
492  P [ ] → (∀l,a. P l → P (l@[a])) →
493   ∀l. P l.
494 #A #P
495qed.*)
496
497lemma rev_preserves_length:
498 ∀A.∀l. length … (rev A l) = length … l.
499  #A #l elim l
500   [ %
501   | #hd #tl #IH normalize >length_append normalize /2/ ]
502qed.
503
504lemma rev_append:
505 ∀A.∀l1,l2.
506  rev A (l1@l2) = rev A l2 @ rev A l1.
507 #A #l1 elim l1 normalize //
508qed.
509
510lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
511 #A #l elim l
512  [ //
513  | #hd #tl #IH normalize >rev_append normalize // ]
514qed.
515
516lemma split_len_Sn:
517 ∀A:Type[0].∀l:list A.∀len.
518  length … l = S len →
519   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
520 #A #l elim l
521  [ normalize #len #abs destruct
522  | #hd #tl #IH #len
523    generalize in match (rev_rev … tl)
524    cases (rev A tl) in ⊢ (??%? → ?)
525     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/
526     | #a #l' #H <H normalize #EQ
527      %[@(hd::rev … l')] %[@a] % //
528      >length_append in EQ #EQ normalize in EQ; normalize;
529      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
530qed.
531
532lemma list_elim_rev:
533 ∀A:Type[0].∀P:list A → Type[0].
534  P [ ] → (∀l,a. P l → P (l@[a])) →
535   ∀l. P l.
536 #A #P #H1 #H2 #l
537 generalize in match (refl … (length … l))
538 generalize in ⊢ (???% → ?) #n generalize in match l
539 elim n
540  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
541  | #m #IH #L #EQ
542    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
543qed.
544
545axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
546axiom prefix_of_append:
547 ∀A:Type[0].∀l,l1,l2:list A.
548  is_prefix … l l1 → is_prefix … l (l1@l2).
549axiom prefix_reflexive: ∀A,l. is_prefix A l l.
550axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
551
552record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
553
554definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
555 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
556
557definition app ≝
558 λA:Type[0].λl1:Propify (list A).λl2:list A.
559  match l1 with
560   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
561
562lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
563 #A * /3/
564qed.
565
566lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
567 #A * #l1 normalize //
568qed.
569
570let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
571 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
572 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
573 B (app … prefix l) ≝
574  match l with
575  [ nil ⇒ ? (* b *)
576  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
577  ].
578 [ applyS b
579 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
580qed.
581
582(*
583let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
584 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
585  match l with
586  [ nil ⇒ ? (* b *)
587  | cons hd tl ⇒
588     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
589  ].
590 [ applyS b
591 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
592qed.
593*)
594
595definition foldll:
596 ∀A:Type[0].∀B: Propify (list A) → Type[0].
597  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
598   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
599 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
600
601axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
602axiom pprefix_of_append:
603 ∀A:Type[0].∀l,l1,l2.
604  is_pprefix A l l1 → is_pprefix A l (l1@l2).
605axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
606axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
607
608
609axiom foldll':
610 ∀A:Type[0].∀l: list A.
611  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
612  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
613   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
614 #A #l #B
615 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
616
617
618  #H #acc
619 @foldll
620  [
621  |
622  ]
623
624 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
625
626
627(*
628record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
629 { subset_wit:> A;
630   subset_proof: P subset_wit
631 }.
632*)
633
634definition build_maps' ≝
635  λpseudo_program.
636  let 〈preamble,instr_list〉 ≝ pseudo_program in
637  let result ≝
638   foldll
639    (option Identifier × pseudo_instruction)
640    (λprefix.
641      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
642       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
643    (λprefix,t,i.
644      let 〈labels, pc_costs〉 ≝ t in
645      let 〈program_counter, costs〉 ≝ pc_costs in
646       let 〈label, i'〉 ≝ i in
647       let labels ≝
648         match label with
649         [ None ⇒ labels
650         | Some label ⇒
651           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
652             insert ? ? label program_counter_bv labels
653         ]
654       in
655         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
656         [ None ⇒
657            let dummy ≝ 〈labels,pc_costs〉 in
658              dummy
659         | Some construct ⇒ 〈labels, construct〉
660         ]
661    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
662  in
663   let 〈labels, pc_costs〉 ≝ result in
664   let 〈pc, costs〉 ≝ pc_costs in
665    〈labels, costs〉.
666 [
667 | @⊥
668 | normalize % //
669 ]
670qed.
671
672definition build_maps' ≝
673  λpseudo_program.
674  let 〈preamble,instr_list〉 ≝ pseudo_program in
675  let result ≝
676   foldl
677    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
678          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
679           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
680    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
681          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
682           is_prefix ? instr_list_prefix' instr_list →
683           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
684    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
685          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
686           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
687     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
688          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
689           is_prefix ? instr_list_prefix' instr_list →
690           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
691      let 〈labels, pc_costs〉 ≝ t in
692      let 〈program_counter, costs〉 ≝ pc_costs in
693       let 〈label, i'〉 ≝ i in
694       let labels ≝
695         match label with
696         [ None ⇒ labels
697         | Some label ⇒
698           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
699             insert ? ? label program_counter_bv labels
700         ]
701       in
702         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
703         [ None ⇒
704            let dummy ≝ 〈labels,pc_costs〉 in
705              dummy
706         | Some construct ⇒ 〈labels, construct〉
707         ]
708    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
709  in
710   let 〈labels, pc_costs〉 ≝ result in
711   let 〈pc, costs〉 ≝ pc_costs in
712    〈labels, costs〉.
713 [4: @(list_elim_rev ?
714       (λinstr_list. list (
715        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
716          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
717           is_prefix ? instr_list_prefix' instr_list →
718           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
719       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
720      [ @[ ]
721      | #l' #a #limage %2
722        [ %[@a] #PREFIX #PREFIX_OK
723        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
724             THE INDUCTION HYPOTHESIS INSTEAD *)
725          elim limage
726           [ %1
727           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
728             @K1 @(prefix_of_append ???? K3)
729           ]
730        ]
731
732
733
734
735  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
736     % [@ (LIST_PREFIX @ [i])] %
737      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
738      | (* DOABLE IN PRINCIPLE *)
739      ]
740 | (* assert false case *)
741 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
742 |
743
744let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
745                       (encoding: list Byte) on encoding: Prop ≝
746  match encoding with
747  [ nil ⇒ final_pc = pc
748  | cons hd tl ⇒
749    let 〈new_pc, byte〉 ≝ next code_memory pc in
750      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
751  ].
752
753definition assembly_specification:
754  ∀assembly_program: pseudo_assembly_program.
755  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
756  λpseudo_assembly_program.
757  λcode_mem.
758    ∀pc: Word.
759      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
760      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
761      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
762      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
763      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
764       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
765      match pre_assembled with
766       [ None ⇒ True
767       | Some pc_code ⇒
768          let 〈new_pc,code〉 ≝ pc_code in
769           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
770
771axiom assembly_meets_specification:
772  ∀pseudo_assembly_program.
773    match assembly pseudo_assembly_program with
774    [ None ⇒ True
775    | Some code_mem_cost ⇒
776      let 〈code_mem, cost〉 ≝ code_mem_cost in
777        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
778    ].
779(*
780  # PROGRAM
781  [ cases PROGRAM
782    # PREAMBLE
783    # INSTR_LIST
784    elim INSTR_LIST
785    [ whd
786      whd in ⊢ (∀_. %)
787      # PC
788      whd
789    | # INSTR
790      # INSTR_LIST_TL
791      # H
792      whd
793      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
794    ]
795  | cases not_implemented
796  ] *)
797
798definition status_of_pseudo_status: PseudoStatus → option Status ≝
799 λps.
800  let pap ≝ code_memory … ps in
801   match assembly pap with
802    [ None ⇒ None …
803    | Some p ⇒
804       let cm ≝ load_code_memory (\fst p) in
805       let pc ≝ sigma' pap (program_counter ? ps) in
806        Some …
807         (mk_PreStatus (BitVectorTrie Byte 16)
808           cm
809           (low_internal_ram … ps)
810           (high_internal_ram … ps)
811           (external_ram … ps)
812           pc
813           (special_function_registers_8051 … ps)
814           (special_function_registers_8052 … ps)
815           (p1_latch … ps)
816           (p3_latch … ps)
817           (clock … ps)) ].
818
819definition write_at_stack_pointer':
820 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
821  λM: Type[0].
822  λs: PreStatus M.
823  λv: Byte.
824    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
825    let bit_zero ≝ get_index_v… nu O ? in
826    let bit_1 ≝ get_index_v… nu 1 ? in
827    let bit_2 ≝ get_index_v… nu 2 ? in
828    let bit_3 ≝ get_index_v… nu 3 ? in
829      if bit_zero then
830        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
831                              v (low_internal_ram ? s) in
832          set_low_internal_ram ? s memory
833      else
834        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
835                              v (high_internal_ram ? s) in
836          set_high_internal_ram ? s memory.
837  [ cases l0 %
838  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
839qed.
840
841definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
842 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
843
844  λticks_of.
845  λs.
846  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
847  let ticks ≝ ticks_of (program_counter ? s) in
848  let s ≝ set_clock ? s (clock ? s + ticks) in
849  let s ≝ set_program_counter ? s pc in
850    match instr with
851    [ Instruction instr ⇒
852       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
853    | Comment cmt ⇒ s
854    | Cost cst ⇒ s
855    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
856    | Call call ⇒
857      let a ≝ address_of_word_labels s call in
858      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
859      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
860      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
861      let s ≝ write_at_stack_pointer' ? s pc_bl in
862      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
863      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
864      let s ≝ write_at_stack_pointer' ? s pc_bu in
865        set_program_counter ? s a
866    | Mov dptr ident ⇒
867       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
868    ].
869 [
870 |2,3,4: %
871 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
872 |
873 | %
874 ]
875 cases not_implemented
876qed.
877
878(*
879lemma execute_code_memory_unchanged:
880 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
881 #ticks #ps whd in ⊢ (??? (??%))
882 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
883  (program_counter pseudo_assembly_program ps)) #instr #pc
884 whd in ⊢ (??? (??%)) cases instr
885  [ #pre cases pre
886     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
887       cases (split ????) #z1 #z2 %
888     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
889       cases (split ????) #z1 #z2 %
890     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
891       cases (split ????) #z1 #z2 %
892     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
893       [ #x1 whd in ⊢ (??? (??%))
894     | *: cases not_implemented
895     ]
896  | #comment %
897  | #cost %
898  | #label %
899  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
900    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
901    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
902    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
903    (* CSC: ??? *)
904  | #dptr #label (* CSC: ??? *)
905  ]
906  cases not_implemented
907qed.
908*)
909
910lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
911 ∀ps,ps': PseudoStatus.
912  code_memory … ps = code_memory … ps' →
913   match status_of_pseudo_status ps with
914    [ None ⇒ status_of_pseudo_status ps' = None …
915    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
916    ].
917 #ps #ps' #H whd in ⊢ (mat
918 ch % with [ _ ⇒ ? | _ ⇒ ? ])
919 generalize in match (refl … (assembly (code_memory … ps)))
920 cases (assembly ?) in ⊢ (???% → %)
921  [ #K whd whd in ⊢ (??%?) <H >K %
922  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
923qed.*)
924
925let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
926  match encoding with
927  [ nil ⇒ True
928  | cons hd tl ⇒
929    let 〈new_pc, byte〉 ≝ next code_memory pc in
930      hd = byte ∧ encoding_check' code_memory new_pc tl
931  ].
932
933(* prove later *)
934axiom test:
935  ∀pc: Word.
936  ∀code_memory: BitVectorTrie Byte 16.
937  ∀i: instruction.
938    let assembled ≝ assembly1 i in
939      encoding_check' code_memory pc assembled →
940        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
941        let 〈instr, pc〉 ≝ instr_pc in
942          instr = i.
943
944lemma main_thm:
945 ∀ticks_of.
946 ∀ps: PseudoStatus.
947  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
948  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
949  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
950  let s' ≝ execute_1 s in
951   s = s'']].
952 #ticks_of #ps
953 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
954 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
955 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
956 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
957
958 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.