source: src/ASM/AssemblyProof.ma @ 855

Last change on this file since 855 was 855, checked in by mulligan, 9 years ago

changes from today

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