source: src/ASM/AssemblyProof.ma @ 856

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