source: src/ASM/AssemblyProof.ma @ 860

Last change on this file since 860 was 860, checked in by sacerdot, 8 years ago

Progress in the proof.

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