Context Navigation

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
1	include "ASM/Assembly.ma".
2	include "ASM/Interpret.ma".
3
4	(* RUSSEL **)
5
6	include "basics/jmeq.ma".
7
8	definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
9	definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
10
11	coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
12	coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
13
14	axiom VOID: Type[0].
15	axiom assert_false: VOID.
16	definition bigbang: ∀A:Type[0].False → VOID → A.
17	#A #abs cases abs
18	qed.
19
20	(coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.)
21
22	lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
23	#A #P #p cases p #w #q @q
24	qed.
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 )
31	definition 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
48	definition 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
57	definition 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
69	axiom policy_ok: ∀p. sigma p ≠ None ….
70
71	axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
72
73	(*
74	definition 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
123	let 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
132	definition 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
150	axiom 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
177	definition 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
198	definition 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 ]
218	qed.
219
220	definition 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
255	qed.
256
257	(*
258	lemma 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
286	qed.
287	*)
288
289	lemma 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: % ] ]
302	qed.*)
303
304	let 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
312	lemma 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
326	lemma 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
367	lemma 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.

Download in other formats:

Original Format