source: src/ASM/AssemblyProof.ma @ 859

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

more added

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