source: src/ASM/AssemblyProof.ma @ 850

Last change on this file since 850 was 850, checked in by sacerdot, 9 years ago

More informative foldl: foldll.

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