source: src/ASM/AssemblyProof.ma @ 847

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

Several bugs fixed in Matita.

File size: 13.3 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
20(*coercion 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: 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 p ≠ None ….
70
71axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
72
73(*
74definition build_maps' ≝
75  λpseudo_program.
76  let 〈preamble,instr_list〉 ≝ pseudo_program in
77  let result ≝
78   foldl
79    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
80          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
81           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
82    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
83          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
84           is_prefix ? instr_list_prefix' instr_list ∧
85           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
86    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
87          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
88           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
89     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
90          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
91           is_prefix ? instr_list_prefix' instr_list ∧
92           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
93      let 〈labels, pc_costs〉 ≝ t in
94      let 〈program_counter, costs〉 ≝ pc_costs in
95       let 〈label, i'〉 ≝ i in
96       let labels ≝
97         match label with
98         [ None ⇒ labels
99         | Some label ⇒
100           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
101             insert ? ? label program_counter_bv labels
102         ]
103       in
104         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
105         [ None ⇒ 〈labels,pc_costs〉 (*assert_false*)
106         | Some construct ⇒ 〈labels, construct〉
107         ]
108    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 (\snd ?(*instr_list*))
109  in
110   let 〈labels, pc_costs〉 ≝ result in
111   let 〈pc, costs〉 ≝ pc_costs in
112    〈labels, costs〉.
113 [ cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
114     % [@ (LIST_PREFIX @ [i])] %
115      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
116      | (* DOABLE IN PRINCIPLE *)
117      ]
118 | (* assert false case *)
119 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
120 |
121*)     
122
123let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
124                       (encoding: list Byte) on encoding: Prop ≝
125  match encoding with
126  [ nil ⇒ final_pc = pc
127  | cons hd tl ⇒
128    let 〈new_pc, byte〉 ≝ next code_memory pc in
129      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
130  ].
131
132definition assembly_specification:
133  ∀assembly_program: pseudo_assembly_program.
134  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
135  λpseudo_assembly_program.
136  λcode_mem.
137    ∀pc: Word.
138      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
139      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
140      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
141      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
142      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
143       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
144      match pre_assembled with
145       [ None ⇒ True
146       | Some pc_code ⇒
147          let 〈new_pc,code〉 ≝ pc_code in
148           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
149
150axiom assembly_meets_specification:
151  ∀pseudo_assembly_program.
152    match assembly pseudo_assembly_program with
153    [ None ⇒ True
154    | Some code_mem_cost ⇒
155      let 〈code_mem, cost〉 ≝ code_mem_cost in
156        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
157    ].
158(*
159  # PROGRAM
160  [ cases PROGRAM
161    # PREAMBLE
162    # INSTR_LIST
163    elim INSTR_LIST
164    [ whd
165      whd in ⊢ (∀_. %)
166      # PC
167      whd
168    | # INSTR
169      # INSTR_LIST_TL
170      # H
171      whd
172      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
173    ]
174  | cases not_implemented
175  ] *)
176
177definition status_of_pseudo_status: PseudoStatus → option Status ≝
178 λps.
179  let pap ≝ code_memory … ps in
180   match assembly pap with
181    [ None ⇒ None …
182    | Some p ⇒
183       let cm ≝ load_code_memory (\fst p) in
184       let pc ≝ sigma' pap (program_counter ? ps) in
185        Some …
186         (mk_PreStatus (BitVectorTrie Byte 16)
187           cm
188           (low_internal_ram … ps)
189           (high_internal_ram … ps)
190           (external_ram … ps)
191           pc
192           (special_function_registers_8051 … ps)
193           (special_function_registers_8052 … ps)
194           (p1_latch … ps)
195           (p3_latch … ps)
196           (clock … ps)) ].
197
198definition write_at_stack_pointer':
199 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
200  λM: Type[0].
201  λs: PreStatus M.
202  λv: Byte.
203    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
204    let bit_zero ≝ get_index_v… nu O ? in
205    let bit_1 ≝ get_index_v… nu 1 ? in
206    let bit_2 ≝ get_index_v… nu 2 ? in
207    let bit_3 ≝ get_index_v… nu 3 ? in
208      if bit_zero then
209        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
210                              v (low_internal_ram ? s) in
211          set_low_internal_ram ? s memory
212      else
213        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
214                              v (high_internal_ram ? s) in
215          set_high_internal_ram ? s memory.
216  [ cases l0 %
217  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
218qed.
219
220definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
221 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
222
223  λticks_of.
224  λs.
225  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
226  let ticks ≝ ticks_of (program_counter ? s) in
227  let s ≝ set_clock ? s (clock ? s + ticks) in
228  let s ≝ set_program_counter ? s pc in
229    match instr with
230    [ Instruction instr ⇒
231       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
232    | Comment cmt ⇒ s
233    | Cost cst ⇒ s
234    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
235    | Call call ⇒
236      let a ≝ address_of_word_labels s call in
237      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
238      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
239      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
240      let s ≝ write_at_stack_pointer' ? s pc_bl in
241      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
242      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
243      let s ≝ write_at_stack_pointer' ? s pc_bu in
244        set_program_counter ? s a
245    | Mov dptr ident ⇒
246       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
247    ].
248 [
249 |2,3,4: %
250 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
251 |
252 | %
253 ]
254 cases not_implemented
255qed.
256
257(*
258lemma execute_code_memory_unchanged:
259 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
260 #ticks #ps whd in ⊢ (??? (??%))
261 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
262  (program_counter pseudo_assembly_program ps)) #instr #pc
263 whd in ⊢ (??? (??%)) cases instr
264  [ #pre cases pre
265     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
266       cases (split ????) #z1 #z2 %
267     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
268       cases (split ????) #z1 #z2 %
269     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
270       cases (split ????) #z1 #z2 %
271     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
272       [ #x1 whd in ⊢ (??? (??%))
273     | *: cases not_implemented
274     ]
275  | #comment %
276  | #cost %
277  | #label %
278  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
279    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
280    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
281    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
282    (* CSC: ??? *)
283  | #dptr #label (* CSC: ??? *)
284  ]
285  cases not_implemented
286qed.
287*)
288
289lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
290 ∀ps,ps': PseudoStatus.
291  code_memory … ps = code_memory … ps' →
292   match status_of_pseudo_status ps with
293    [ None ⇒ status_of_pseudo_status ps' = None …
294    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
295    ].
296 #ps #ps' #H whd in ⊢ (mat
297 ch % with [ _ ⇒ ? | _ ⇒ ? ])
298 generalize in match (refl … (assembly (code_memory … ps)))
299 cases (assembly ?) in ⊢ (???% → %)
300  [ #K whd whd in ⊢ (??%?) <H >K %
301  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
302qed.*)
303
304let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
305  match encoding with
306  [ nil ⇒ True
307  | cons hd tl ⇒
308    let 〈new_pc, byte〉 ≝ next code_memory pc in
309      hd = byte ∧ encoding_check' code_memory new_pc tl
310  ].
311
312lemma test:
313  ∀i: instruction.
314  ∃pc.
315  let assembled ≝ assembly1 i in
316  let code_memory ≝ load_code_memory assembled in
317  let fetched ≝ fetch code_memory pc in
318  let 〈instr_pc, ticks〉 ≝ fetched in
319    \fst instr_pc = i.
320  # INSTR
321  %
322  [ @ (zero 16)
323  | cases INSTR
324  ].
325
326lemma test:
327  ∀pc: Word.
328  ∀code_memory: BitVectorTrie Byte 16.
329  ∀i: instruction.
330    let assembled ≝ assembly1 i in
331      encoding_check' code_memory pc assembled →
332        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
333        let 〈instr, pc〉 ≝ instr_pc in
334          instr = i.
335  # PC # CODE_MEMORY # INSTRUCTION
336  whd
337  whd in ⊢ (? → match % with [ _ ⇒ ? ])
338  cases (next CODE_MEMORY PC)
339  whd
340  # PC1 # V1
341
342
343  cases (fetch CODE_MEMORY PC)
344  # INSTR_PC
345  # TICKS
346  cases (INSTRUCTION)
347  [ # ADDR11
348    # ENCODING_CHECK
349    whd in ENCODING_CHECK;
350    normalize
351    cases (INSTR_PC)
352    # INSTR
353    # PC
354    normalize
355   
356   
357  # ENCODING
358  normalize
359  [ cases INSTR_PC
360    # NEW_INSTRUCTION
361    # PC
362    normalize
363    normalize in ENCODING;
364  | # ASSEMBLED
365    whd
366 
367lemma main_thm:
368 ∀ticks_of.
369 ∀ps: PseudoStatus.
370  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
371  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
372  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
373  let s' ≝ execute_1 s in
374   s = s'']].
375 #ticks_of #ps
376 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
377 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
378 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
379 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
380 
381 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.