Context Navigation

AssemblyProof.ma @ 851

Last change on this file since 851 was 851, checked in by mulligan, 8 years ago
strong foldl added
File size: 22.0 KB

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