source: src/ASM/AssemblyProof.ma @ 846

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

changes

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