source: src/ASM/AssemblyProof.ma @ 852

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

foldl_strong outer definition

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