source: src/ASM/AssemblyProof.ma @ 854

Last change on this file since 854 was 854, checked in by mulligan, 10 years ago

commit to avoid conflicts

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