Context Navigation

AssemblyProof.ma @ 854

Last change on this file since 854 was 854, checked in by mulligan, 10 years ago
commit to avoid conflicts
File size: 25.3 KB

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