Context Navigation

AssemblyProof.ma @ 2197

Last change on this file since 2197 was 2197, checked in by sacerdot, 8 years ago
Main lemmas all closed.
File size: 49.3 KB

Line
1	include "ASM/Assembly.ma".
2	include "ASM/Interpret.ma".
3	include "ASM/StatusProofs.ma".
4	include alias "arithmetics/nat.ma".
5
6	let rec encoding_check
7	(code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
8	(encoding: list Byte)
9	on encoding: Prop ≝
10	match encoding with
11	[ nil ⇒ final_pc = pc
12	\| cons hd tl ⇒
13	let 〈new_pc, byte〉 ≝ next code_memory pc in
14	hd = byte ∧ encoding_check code_memory new_pc final_pc tl
15	].
16
17	lemma encoding_check_append:
18	∀code_memory: BitVectorTrie Byte 16.
19	∀final_pc: Word.
20	∀l1: list Byte.
21	∀pc: Word.
22	∀l2: list Byte.
23	encoding_check code_memory pc final_pc (l1@l2) →
24	let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
25	encoding_check code_memory pc pc_plus_len l1 ∧
26	encoding_check code_memory pc_plus_len final_pc l2.
27	#code_memory #final_pc #l1 elim l1
28	[1:
29	#pc #l2
30	whd in ⊢ (????% → ?); #H
31	<add_zero
32	whd whd in ⊢ (?%?); /2/
33	\|2:
34	#hd #tl #IH #pc #l2 * #H1 #H2
35	(* >add_SO in H2; #H2 *)
36	cases (IH … H2) #E1 #E2 %
37	[1:
38	% try @H1
39	<(add_bitvector_of_nat_Sm 16 (\|tl\|)) in E1;
40	<add_associative #assm assumption
41	\|2:
42	<add_associative in E2;
43	<(add_bitvector_of_nat_Sm 16 (\|tl\|)) #assm
44	assumption
45	]
46	]
47	qed.
48
49	definition ticks_of_instruction ≝
50	λi.
51	let trivial_code_memory ≝ assembly1 i in
52	let trivial_status ≝ load_code_memory trivial_code_memory in
53	\snd (fetch trivial_status (zero ?)).
54
55	lemma fetch_assembly:
56	∀pc: Word.
57	∀i: instruction.
58	∀code_memory: BitVectorTrie Byte 16.
59	∀assembled: list Byte.
60	assembled = assembly1 i →
61	let len ≝ length … assembled in
62	let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
63	encoding_check code_memory pc pc_plus_len assembled →
64	let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
65	(eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
66	cases daemon
67	(* XXX: commented out as takes ages to typecheck
68	#pc #i #code_memory #assembled cases i [8: *]
69	[16,20,29: * * \|18,19: * * [1,2,4,5: ] \|28: * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
70	[47,48,49:
71	\|*: #arg @(subaddressing_mode_elim … arg)
72	[2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58,
73	59,60,63,64,65,66,67: #ARG]]
74	[4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
75	56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
76	[1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
77	39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
78	68,69,70,71: #ARG2]]
79	[1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
80	normalize in ⊢ (???% → ?);
81	[92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
82	normalize in ⊢ (???% → ?);]
83	#H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
84	try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
85	whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
86	[17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
87	try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
88	qed.
89
90	let rec fetch_many
91	(code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
92	(expected: list instruction)
93	on expected: Prop ≝
94	match expected with
95	[ nil ⇒ eq_bv … pc final_pc = true
96	\| cons i tl ⇒
97	let pc' ≝ add 16 pc (bitvector_of_nat 16 (\|assembly1 … i\|)) in
98	(〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
99	fetch_many code_memory final_pc pc' tl)
100	].
101
102	lemma fetch_assembly_pseudo':
103	∀lookup_labels.
104	∀sigma: Word → Word.
105	∀policy: Word → bool.
106	∀ppc.
107	∀lookup_datalabels.
108	∀pi.
109	∀code_memory.
110	∀len.
111	∀assembled.
112	∀instructions.
113	let pc ≝ sigma ppc in
114	instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
115	〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
116	let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
117	encoding_check code_memory pc pc_plus_len assembled →
118	fetch_many code_memory pc_plus_len pc instructions.
119	#lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
120	normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
121	cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
122	>len_refl >assembled_refl -len_refl
123	generalize in match (add 16 (sigma ppc)
124	(bitvector_of_nat 16
125	(\|flatten (Vector bool 8)
126	(map instruction (list (Vector bool 8)) assembly1 instructions)\|)));
127	#final_pc
128	generalize in match (sigma ppc); elim instructions
129	[1:
130	#pc whd in ⊢ (% → %); #H >H @eq_bv_refl
131	\|2:
132	#i #tl #IH #pc #H whd
133	cases (encoding_check_append ????? H) -H #H1 #H2
134	lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
135	cases (fetch ??) * #instr #pc' #ticks
136	#H3 lapply (H3 H1) -H3 normalize nodelta #H3
137	lapply (conjunction_true ?? H3) * #H4 #H5
138	lapply (conjunction_true … H4) * #B1 #B2
139	>(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
140	>(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
141	]
142	qed.
143
144	lemma fetch_assembly_pseudo:
145	∀program: pseudo_assembly_program.
146	∀sigma: Word → Word.
147	∀policy: Word → bool.
148	let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
149	let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
150	∀ppc.∀ppc_ok.
151	∀code_memory.
152	let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst program)) x (zero 16) in
153	let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
154	let pc ≝ sigma ppc in
155	let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
156	let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
157	let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
158	encoding_check code_memory pc pc_plus_len assembled →
159	fetch_many code_memory pc_plus_len pc instructions.
160	#program #sigma #policy
161	@pair_elim #labels #costs #create_label_cost_map_refl
162	letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
163	letin lookup_datalabels ≝ (λx.?)
164	letin pi ≝ (fst ???)
165	letin pc ≝ (sigma ?)
166	letin instructions ≝ (expand_pseudo_instruction ??????)
167	@pair_elim #len #assembled #assembled_refl normalize nodelta
168	#H
169	generalize in match
170	(fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
171	#X destruct normalize nodelta @X try % <assembled_refl try % assumption
172	qed.
173
174	definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
175	λpseudo_instruction.
176	match pseudo_instruction with
177	[ Comment c ⇒ False
178	\| Cost c ⇒ False
179	\| _ ⇒ True
180	].
181
182	(* This is a non trivial consequence of fetch_assembly_pseudo +
183	load_code_memory_ok because of the finite amount of memory. In
184	particular the case when the compiled program exhausts the
185	code memory is very tricky. It also requires monotonicity of
186	sigma in the out-of-bounds region too. *)
187	lemma assembly_ok:
188	∀program.
189	∀length_proof: \|\snd program\| ≤ 2^16.
190	∀sigma: Word → Word.
191	∀policy: Word → bool.
192	∀sigma_policy_witness: sigma_policy_specification program sigma policy.
193	∀assembled.
194	∀costs': BitVectorTrie costlabel 16.
195	let 〈preamble, instr_list〉 ≝ program in
196	let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
197	let datalabels ≝ construct_datalabels preamble in
198	let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
199	〈assembled,costs'〉 = assembly program sigma policy →
200	(* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
201	let code_memory ≝ load_code_memory assembled in
202	let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
203	∀ppc.∀ppc_ok.
204	let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
205	let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
206	let pc ≝ sigma ppc in
207	let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
208	encoding_check code_memory pc pc_plus_len assembled ∧
209	sigma newppc = add … pc (bitvector_of_nat … len).
210	#program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
211	cases (assembly program sigma policy) * #assembled' #costs''
212	@pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
213	cut (\|instr_list\| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
214	#H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
215	@pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
216	* * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
217	#ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
218	@pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
219	lapply (assembly_ok2 ppc ?) try // -assembly_ok2
220	>eq_fetch_pseudo_instruction
221	change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<\|assembledi\|.?) → ?)
222	>eq_assembly_1_pseudoinstruction
223	whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
224	%
225	[2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
226	>snd_fetch_pseudo_instruction
227	cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
228	#spw1 #_ >spw1 -spw1 @eq_f @eq_f
229	>eq_fetch_pseudo_instruction whd in match instruction_size;
230	normalize nodelta >create_label_cost_refl
231	>fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
232	[>eq_assembly_1_pseudoinstruction % \| skip]
233	\| lapply (load_code_memory_ok assembled' ?) [ assumption ]
234	#load_code_memory_ok
235	lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
236	(* Nice statement here *)
237	cut (∀j. ∀H: j < \|assembled\|.
238	nth_safe Byte j assembled H =
239	\snd (next (load_code_memory assembled')
240	(bitvector_of_nat 16
241	(nat_of_bitvector …
242	(add … (sigma ppc) (bitvector_of_nat … j))))))
243	[1: #j #H cases (assembly_ok … H) #K -assembly_ok #assembly_ok <load_code_memory_ok
244	[ @assembly_ok \| skip ]
245	\|2:
246	-assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
247	elim assembled
248	[1:
249	#pc #_ whd <add_zero %
250	\| #hd #tl #IH #pc #H %
251	[ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
252	>H -H whd in ⊢ (??%?); <add_zero //
253	\| >(?: add … pc (bitvector_of_nat … (S (\|tl\|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (\|tl\|)))
254	[2: <add_bitvector_of_nat_Sm @add_associative ]
255	@IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
256	<(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
257	>add_associative % ]]]]
258	qed.
259
260	(* XXX: should we add that costs = costs'? *)
261	lemma fetch_assembly_pseudo2:
262	∀program.
263	∀length_proof: \|\snd program\| ≤ 2^16.
264	∀sigma.
265	∀policy.
266	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
267	∀ppc.∀ppc_ok.
268	let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
269	let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
270	let code_memory ≝ load_code_memory assembled in
271	let data_labels ≝ construct_datalabels (\fst program) in
272	let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
273	let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
274	let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
275	let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
276	fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
277	* #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
278	@pair_elim #labels #costs #create_label_map_refl
279	@pair_elim #assembled #costs' #assembled_refl
280	letin code_memory ≝ (load_code_memory ?)
281	letin data_labels ≝ (construct_datalabels ?)
282	letin lookup_labels ≝ (λx. ?)
283	letin lookup_datalabels ≝ (λx. ?)
284	@pair_elim #pi #newppc #fetch_pseudo_refl
285	lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
286	normalize nodelta try assumption
287	>create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
288	lapply (H (sym_eq … assembled_refl)) -H
289	lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
290	cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
291	#len #assembledi #EQ4 #H
292	lapply (H ppc) >fetch_pseudo_refl #H
293	lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
294	>create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
295	>EQ4 #H1 cases (H ppc_ok)
296	#H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
297	>fetch_pseudo_refl in H1; #assm @assm assumption
298	qed.
299
300	inductive upper_lower: Type[0] ≝
301	\| upper: upper_lower
302	\| lower: upper_lower.
303
304	definition eq_upper_lower:
305	upper_lower → upper_lower → bool ≝
306	λleft: upper_lower.
307	λright: upper_lower.
308	match left with
309	[ upper ⇒
310	match right with
311	[ upper ⇒ true
312	\| _ ⇒ false
313	]
314	\| lower ⇒
315	match right with
316	[ lower ⇒ true
317	\| _ ⇒ false
318	]
319	].
320
321	lemma eq_upper_lower_true_to_eq:
322	∀left: upper_lower.
323	∀right: upper_lower.
324	eq_upper_lower left right = true → left = right.
325	* * normalize try (#_ %)
326	#absurd destruct(absurd)
327	qed.
328
329	lemma eq_upper_lower_false_to_neq:
330	∀left: upper_lower.
331	∀right: upper_lower.
332	eq_upper_lower left right = false → left ≠ right.
333	* * normalize try (#absurd destruct(absurd))
334	@nmk #absurd destruct(absurd)
335	qed.
336
337	inductive accumulator_address_map_entry: Type[0] ≝
338	\| data: accumulator_address_map_entry
339	\| address: upper_lower → Word → accumulator_address_map_entry.
340
341	definition eq_accumulator_address_map_entry:
342	accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
343	λleft: accumulator_address_map_entry.
344	λright: accumulator_address_map_entry.
345	match left with
346	[ data ⇒
347	match right with
348	[ data ⇒ true
349	\| _ ⇒ false
350	]
351	\| address upper_lower word ⇒
352	match right with
353	[ address upper_lower' word' ⇒
354	eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
355	\| _ ⇒ false
356	]
357	].
358
359	lemma eq_accumulator_address_map_entry_true_to_eq:
360	∀left: accumulator_address_map_entry.
361	∀right: accumulator_address_map_entry.
362	eq_accumulator_address_map_entry left right = true → left = right.
363	#left #right cases left cases right
364	[1:
365	#_ %
366	\|2,3:
367	#upper_lower #word normalize #absurd destruct(absurd)
368	\|4:
369	#upper_lower #word #upper_lower' #word' normalize
370	cases upper_lower' normalize nodelta
371	cases upper_lower normalize
372	[2,3:
373	#absurd destruct(absurd)
374	]
375	change with (eq_bv 16 ?? = true → ?)
376	#relevant lapply (eq_bv_eq … relevant)
377	#word_refl >word_refl %
378	]
379	qed.
380
381	lemma eq_bv_false_to_neq:
382	∀n: nat.
383	∀left, right: BitVector n.
384	eq_bv n left right = false → left ≠ right.
385	#n #left elim left
386	[1:
387	#right >(BitVector_O … right) normalize #absurd destruct(absurd)
388	\|2:
389	#n' #hd #tl #inductive_hypothesis #right
390	cases (BitVector_Sn … right) #hd' * #tl' #right_refl
391	>right_refl normalize
392	cases hd normalize nodelta
393	cases hd' normalize nodelta
394	[2,3:
395	#_ @nmk #absurd destruct(absurd)
396	]
397	change with (eq_bv ??? = false → ?)
398	#relevant lapply (inductive_hypothesis … relevant)
399	#tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
400	#tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
401	]
402	qed.
403
404	lemma eq_accumulator_address_map_entry_false_to_neq:
405	∀left: accumulator_address_map_entry.
406	∀right: accumulator_address_map_entry.
407	eq_accumulator_address_map_entry left right = false → left ≠ right.
408	#left #right cases left cases right
409	[1:
410	normalize #absurd destruct(absurd)
411	\|2,3:
412	#upper_lower #word normalize #_
413	@nmk #absurd destruct(absurd)
414	\|4:
415	#upper_lower #word #upper_lower' #word' normalize
416	cases upper_lower' normalize nodelta
417	cases upper_lower normalize nodelta
418	[2,3:
419	#_ @nmk #absurd destruct(absurd)
420	]
421	change with (eq_bv ??? = false → ?)
422	#eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
423	#word_neq_assm @nmk #address_eq_assm cases word_neq_assm
424	#word_eq_assm @word_eq_assm destruct(address_eq_assm) %
425	]
426	qed.
427
428	(* XXX: changed this type. Bool specifies whether byte is first or second
429	component of an address, and the Word is the pseudoaddress that it
430	corresponds to. Second component is the same principle for the accumulator
431	A.
432	*)
433	definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
434
435	include alias "ASM/BitVectorTrie.ma".
436
437	include "common/AssocList.ma".
438
439	axiom low_internal_ram_of_pseudo_low_internal_ram:
440	∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
441
442	axiom high_internal_ram_of_pseudo_high_internal_ram:
443	∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
444
445	axiom low_internal_ram_of_pseudo_internal_ram_hit:
446	∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
447	assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 →
448	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
449	let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
450	let bl ≝ lookup ? 7 addr ram (zero 8) in
451	let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
452	let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
453	if eq_upper_lower upper_lower upper then
454	(pbl = higher) ∧ (bl = phigher)
455	else
456	(pbl = lower) ∧ (bl = plower).
457
458	(* changed from add to sub *)
459	axiom low_internal_ram_of_pseudo_internal_ram_miss:
460	∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
461	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
462	assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
463	lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
464
465	definition addressing_mode_ok ≝
466	λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
467	λaddr:addressing_mode.
468	match addr with
469	[ DIRECT d ⇒
470	if eq_bv … d (bitvector_of_nat … 224) then
471	¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
472	else
473	¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
474	\| INDIRECT i ⇒
475	let d ≝ get_register … s [[false;false;i]] in
476	¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
477	\| EXT_INDIRECT _ ⇒ true
478	\| REGISTER r ⇒
479	let address ≝ bit_address_of_register … s r in
480	¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
481	\| ACC_A ⇒ match \snd M with [ data ⇒ true \| _ ⇒ false ]
482	\| ACC_B ⇒ true
483	\| DPTR ⇒ true
484	\| DATA _ ⇒ true
485	\| DATA16 _ ⇒ true
486	\| ACC_DPTR ⇒ true
487	\| ACC_PC ⇒ true
488	\| EXT_INDIRECT_DPTR ⇒ true
489	\| INDIRECT_DPTR ⇒ true
490	\| CARRY ⇒ true
491	\| BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
492	\| N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
493	\| RELATIVE _ ⇒ true
494	\| ADDR11 _ ⇒ true
495	\| ADDR16 _ ⇒ true
496	].
497
498	definition next_internal_pseudo_address_map0 ≝
499	λT.
500	λcm:T.
501	λaddr_of: Identifier → PreStatus T cm → Word.
502	λfetched.
503	λM: internal_pseudo_address_map.
504	λs: PreStatus T cm.
505	match fetched with
506	[ Comment _ ⇒ Some ? M
507	\| Cost _ ⇒ Some … M
508	\| Jmp _ ⇒ Some … M
509	\| Call a ⇒
510	let a' ≝ addr_of a s in
511	let 〈callM, accM〉 ≝ M in
512	Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
513	〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
514	\| Mov _ _ ⇒ Some … M
515	\| Instruction instr ⇒
516	match instr return λx. option internal_pseudo_address_map with
517	[ ADD addr1 addr2 ⇒
518	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
519	Some ? M
520	else
521	None ?
522	\| ADDC addr1 addr2 ⇒
523	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
524	Some ? M
525	else
526	None ?
527	\| SUBB addr1 addr2 ⇒
528	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
529	Some ? M
530	else
531	None ?
532	\| INC addr1 ⇒
533	if addressing_mode_ok T M ? s addr1 then
534	Some ? M
535	else
536	None ?
537	\| DEC addr1 ⇒
538	if addressing_mode_ok T M … s addr1 then
539	Some ? M
540	else
541	None ?
542	\| MUL addr1 addr2 ⇒
543	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
544	Some ? M
545	else
546	None ?
547	\| DIV addr1 addr2 ⇒
548	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
549	Some ? M
550	else
551	None ?
552	\| DA addr1 ⇒
553	if addressing_mode_ok T M … s addr1 then
554	Some ? M
555	else
556	None ?
557	\| JC addr1 ⇒ Some ? M
558	\| JNC addr1 ⇒ Some ? M
559	\| JB addr1 addr2 ⇒ Some ? M
560	\| JNB addr1 addr2 ⇒ Some ? M
561	\| JBC addr1 addr2 ⇒ Some ? M
562	\| JZ addr1 ⇒ Some ? M
563	\| JNZ addr1 ⇒ Some ? M
564	\| CJNE addr1 addr2 ⇒
565	match addr1 with
566	[ inl l ⇒
567	let 〈left, right〉 ≝ l in
568	if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
569	Some ? M
570	else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
571	Some ? M
572	else
573	None ?
574	\| inr r ⇒
575	let 〈left, right〉 ≝ r in
576	if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
577	Some ? M
578	else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
579	Some ? M
580	else
581	None ?
582	]
583	\| DJNZ addr1 addr2 ⇒
584	if addressing_mode_ok T M … s addr1 then
585	Some ? M
586	else
587	None ?
588	\| CLR addr1 ⇒
589	if addressing_mode_ok T M … s addr1 then
590	Some ? M
591	else
592	None ?
593	\| CPL addr1 ⇒
594	if addressing_mode_ok T M … s addr1 then
595	Some ? M
596	else
597	None ?
598	\| RL addr1 ⇒
599	if addressing_mode_ok T M … s addr1 then
600	Some ? M
601	else
602	None ?
603	\| RLC addr1 ⇒
604	if addressing_mode_ok T M … s addr1 then
605	Some ? M
606	else
607	None ?
608	\| RR addr1 ⇒
609	if addressing_mode_ok T M … s addr1 then
610	Some ? M
611	else
612	None ?
613	\| RRC addr1 ⇒
614	if addressing_mode_ok T M … s addr1 then
615	Some ? M
616	else
617	None ?
618	\| SWAP addr1 ⇒
619	if addressing_mode_ok T M … s addr1 then
620	Some ? M
621	else
622	None ?
623	\| SETB addr1 ⇒
624	if addressing_mode_ok T M … s addr1 then
625	Some ? M
626	else
627	None ?
628	(* XXX: need to track addresses pushed and popped off the stack? *)
629	\| PUSH addr1 ⇒
630	let 〈callM, accM〉 ≝ M in
631	match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
632	[ DIRECT d ⇒ λproof.
633	let extended ≝ pad 8 8 d in
634	Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
635	\| _ ⇒ λother: False. ⊥
636	] (subaddressing_modein … addr1)
637	\| POP addr1 ⇒ Some … M
638	\| XCH addr1 addr2 ⇒
639	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
640	Some ? M
641	else
642	None ?
643	\| XCHD addr1 addr2 ⇒
644	if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
645	Some ? M
646	else
647	None ?
648	\| RET ⇒
649	let 〈callM, accM〉 ≝ M in
650	let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
651	let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
652	if sp_plus_1 ∧ sp_plus_2 then
653	Some … M
654	else
655	None ?
656	\| RETI ⇒
657	let 〈callM, accM〉 ≝ M in
658	let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
659	let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
660	if sp_plus_1 ∧ sp_plus_2 then
661	Some … M
662	else
663	None ?
664	\| NOP ⇒ Some … M
665	\| MOVX addr1 ⇒ Some … M
666	\| XRL addr1 ⇒
667	match addr1 with
668	[ inl l ⇒
669	let 〈acc_a, others〉 ≝ l in
670	let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
671	let others_ok ≝ addressing_mode_ok T M … s others in
672	if acc_a_ok ∧ others_ok then
673	Some ? M
674	else
675	None ?
676	\| inr r ⇒
677	let 〈direct, others〉 ≝ r in
678	let direct_ok ≝ addressing_mode_ok T M … s direct in
679	let others_ok ≝ addressing_mode_ok T M … s others in
680	if direct_ok ∧ others_ok then
681	Some ? M
682	else
683	None ?
684	]
685	\| ORL addr1 ⇒
686	match addr1 with
687	[ inl l ⇒
688	match l with
689	[ inl l ⇒
690	let 〈acc_a, others〉 ≝ l in
691	let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
692	let others_ok ≝ addressing_mode_ok T M … s others in
693	if acc_a_ok ∧ others_ok then
694	Some ? M
695	else
696	None ?
697	\| inr r ⇒
698	let 〈direct, others〉 ≝ r in
699	let direct_ok ≝ addressing_mode_ok T M … s direct in
700	let others_ok ≝ addressing_mode_ok T M … s others in
701	if direct_ok ∧ others_ok then
702	Some ? M
703	else
704	None ?
705	]
706	\| inr r ⇒
707	let 〈carry, others〉 ≝ r in
708	let carry_ok ≝ addressing_mode_ok T M … s carry in
709	let others_ok ≝ addressing_mode_ok T M … s others in
710	if carry_ok ∧ others_ok then
711	Some ? M
712	else
713	None ?
714	]
715	\| ANL addr1 ⇒
716	match addr1 with
717	[ inl l ⇒
718	match l with
719	[ inl l ⇒
720	let 〈acc_a, others〉 ≝ l in
721	let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
722	let others_ok ≝ addressing_mode_ok T M … s others in
723	if acc_a_ok ∧ others_ok then
724	Some ? M
725	else
726	None ?
727	\| inr r ⇒
728	let 〈direct, others〉 ≝ r in
729	let direct_ok ≝ addressing_mode_ok T M … s direct in
730	let others_ok ≝ addressing_mode_ok T M … s others in
731	if direct_ok ∧ others_ok then
732	Some ? M
733	else
734	None ?
735	]
736	\| inr r ⇒
737	let 〈carry, others〉 ≝ r in
738	let carry_ok ≝ addressing_mode_ok T M … s carry in
739	let others_ok ≝ addressing_mode_ok T M … s others in
740	if carry_ok ∧ others_ok then
741	Some ? M
742	else
743	None ?
744	]
745	\| MOV addr1 ⇒ Some … M
746	]
747	].
748	cases other
749	qed.
750
751	definition next_internal_pseudo_address_map ≝
752	λM:internal_pseudo_address_map.
753	λcm.
754	λaddr_of.
755	λs:PseudoStatus cm.
756	λppc_ok.
757	next_internal_pseudo_address_map0 ? cm addr_of
758	(\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
759
760	definition code_memory_of_pseudo_assembly_program:
761	∀pap:pseudo_assembly_program.
762	(Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
763	λpap.
764	λsigma.
765	λpolicy.
766	let p ≝ pi1 … (assembly pap sigma policy) in
767	load_code_memory (\fst p).
768
769	definition sfr_8051_of_pseudo_sfr_8051 ≝
770	λM: internal_pseudo_address_map.
771	λsfrs: Vector Byte 19.
772	λsigma: Word → Word.
773	match \snd M with
774	[ data ⇒ sfrs
775	\| address upper_lower address ⇒
776	let index ≝ sfr_8051_index SFR_ACC_A in
777	let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
778	if eq_upper_lower upper_lower upper then
779	set_index Byte 19 sfrs index high ?
780	else
781	set_index Byte 19 sfrs index low ?
782	].
783	//
784	qed.
785
786	definition status_of_pseudo_status:
787	internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
788	∀sigma: Word → Word. ∀policy: Word → bool.
789	Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
790	λM.
791	λpap.
792	λps.
793	λsigma.
794	λpolicy.
795	let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
796	let pc ≝ sigma (program_counter … ps) in
797	let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
798	let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
799	mk_PreStatus (BitVectorTrie Byte 16)
800	cm
801	lir
802	hir
803	(external_ram … ps)
804	pc
805	(sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
806	(special_function_registers_8052 … ps)
807	(p1_latch … ps)
808	(p3_latch … ps)
809	(clock … ps).
810
811	(*
812	definition write_at_stack_pointer':
813	∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
814	λM: Type[0].
815	λs: PreStatus M.
816	λv: Byte.
817	let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
818	let bit_zero ≝ get_index_v… nu O ? in
819	let bit_1 ≝ get_index_v… nu 1 ? in
820	let bit_2 ≝ get_index_v… nu 2 ? in
821	let bit_3 ≝ get_index_v… nu 3 ? in
822	if bit_zero then
823	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
824	v (low_internal_ram ? s) in
825	set_low_internal_ram ? s memory
826	else
827	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
828	v (high_internal_ram ? s) in
829	set_high_internal_ram ? s memory.
830	[ cases l0 %
831	\|2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
832	qed.
833
834	definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
835	Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
836	≝
837	λticks_of.
838	λs.
839	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
840	let ticks ≝ ticks_of (program_counter ? s) in
841	let s ≝ set_clock ? s (clock ? s + ticks) in
842	let s ≝ set_program_counter ? s pc in
843	match instr with
844	[ Instruction instr ⇒
845	execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
846	\| Comment cmt ⇒ s
847	\| Cost cst ⇒ s
848	\| Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
849	\| Call call ⇒
850	let a ≝ address_of_word_labels s call in
851	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
852	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
853	let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
854	let s ≝ write_at_stack_pointer' ? s pc_bl in
855	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
856	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
857	let s ≝ write_at_stack_pointer' ? s pc_bu in
858	set_program_counter ? s a
859	\| Mov dptr ident ⇒
860	set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
861	].
862	[
863	\|2,3,4: %
864	\| <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
865	\|
866	\| %
867	]
868	cases not_implemented
869	qed.
870	*)
871
872	(*
873	lemma execute_code_memory_unchanged:
874	∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
875	#ticks #ps whd in ⊢ (??? (??%))
876	cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
877	(program_counter pseudo_assembly_program ps)) #instr #pc
878	whd in ⊢ (??? (??%)) cases instr
879	[ #pre cases pre
880	[ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
881	cases (vsplit ????) #z1 #z2 %
882	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
883	cases (vsplit ????) #z1 #z2 %
884	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
885	cases (vsplit ????) #z1 #z2 %
886	\| #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
887	[ #x1 whd in ⊢ (??? (??%))
888	\| *: cases not_implemented
889	]
890	\| #comment %
891	\| #cost %
892	\| #label %
893	\| #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
894	cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
895	whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
896	whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
897	(* CSC: ??? *)
898	\| #dptr #label (* CSC: ??? *)
899	]
900	cases not_implemented
901	qed.
902	*)
903
904	(* XXX: check values returned for conditional jumps below! They are wrong,
905	find correct values *)
906	definition ticks_of0:
907	∀p:pseudo_assembly_program.
908	(Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
909	λprogram: pseudo_assembly_program.
910	λlookup_labels: Identifier → Word.
911	λsigma.
912	λpolicy.
913	λppc: Word.
914	λfetched.
915	match fetched with
916	[ Instruction instr ⇒
917	match instr with
918	[ JC lbl ⇒
919	let lookup_address ≝ sigma (lookup_labels lbl) in
920	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
921	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
922	if sj_possible then
923	〈2, 2〉
924	else
925	〈4, 4〉
926	\| JNC lbl ⇒
927	let lookup_address ≝ sigma (lookup_labels lbl) in
928	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
929	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
930	if sj_possible then
931	〈2, 2〉
932	else
933	〈4, 4〉
934	\| JB bit lbl ⇒
935	let lookup_address ≝ sigma (lookup_labels lbl) in
936	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
937	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
938	if sj_possible then
939	〈2, 2〉
940	else
941	〈4, 4〉
942	\| JNB bit lbl ⇒
943	let lookup_address ≝ sigma (lookup_labels lbl) in
944	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
945	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
946	if sj_possible then
947	〈2, 2〉
948	else
949	〈4, 4〉
950	\| JBC bit lbl ⇒
951	let lookup_address ≝ sigma (lookup_labels lbl) in
952	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
953	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
954	if sj_possible then
955	〈2, 2〉
956	else
957	〈4, 4〉
958	\| JZ lbl ⇒
959	let lookup_address ≝ sigma (lookup_labels lbl) in
960	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
961	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
962	if sj_possible then
963	〈2, 2〉
964	else
965	〈4, 4〉
966	\| JNZ lbl ⇒
967	let lookup_address ≝ sigma (lookup_labels lbl) in
968	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
969	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
970	if sj_possible then
971	〈2, 2〉
972	else
973	〈4, 4〉
974	\| CJNE arg lbl ⇒
975	let lookup_address ≝ sigma (lookup_labels lbl) in
976	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
977	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
978	if sj_possible then
979	〈2, 2〉
980	else
981	〈4, 4〉
982	\| DJNZ arg lbl ⇒
983	let lookup_address ≝ sigma (lookup_labels lbl) in
984	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
985	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
986	if sj_possible then
987	〈2, 2〉
988	else
989	〈4, 4〉
990	\| ADD arg1 arg2 ⇒
991	let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
992	〈ticks, ticks〉
993	\| ADDC arg1 arg2 ⇒
994	let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
995	〈ticks, ticks〉
996	\| SUBB arg1 arg2 ⇒
997	let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
998	〈ticks, ticks〉
999	\| INC arg ⇒
1000	let ticks ≝ ticks_of_instruction (INC ? arg) in
1001	〈ticks, ticks〉
1002	\| DEC arg ⇒
1003	let ticks ≝ ticks_of_instruction (DEC ? arg) in
1004	〈ticks, ticks〉
1005	\| MUL arg1 arg2 ⇒
1006	let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1007	〈ticks, ticks〉
1008	\| DIV arg1 arg2 ⇒
1009	let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1010	〈ticks, ticks〉
1011	\| DA arg ⇒
1012	let ticks ≝ ticks_of_instruction (DA ? arg) in
1013	〈ticks, ticks〉
1014	\| ANL arg ⇒
1015	let ticks ≝ ticks_of_instruction (ANL ? arg) in
1016	〈ticks, ticks〉
1017	\| ORL arg ⇒
1018	let ticks ≝ ticks_of_instruction (ORL ? arg) in
1019	〈ticks, ticks〉
1020	\| XRL arg ⇒
1021	let ticks ≝ ticks_of_instruction (XRL ? arg) in
1022	〈ticks, ticks〉
1023	\| CLR arg ⇒
1024	let ticks ≝ ticks_of_instruction (CLR ? arg) in
1025	〈ticks, ticks〉
1026	\| CPL arg ⇒
1027	let ticks ≝ ticks_of_instruction (CPL ? arg) in
1028	〈ticks, ticks〉
1029	\| RL arg ⇒
1030	let ticks ≝ ticks_of_instruction (RL ? arg) in
1031	〈ticks, ticks〉
1032	\| RLC arg ⇒
1033	let ticks ≝ ticks_of_instruction (RLC ? arg) in
1034	〈ticks, ticks〉
1035	\| RR arg ⇒
1036	let ticks ≝ ticks_of_instruction (RR ? arg) in
1037	〈ticks, ticks〉
1038	\| RRC arg ⇒
1039	let ticks ≝ ticks_of_instruction (RRC ? arg) in
1040	〈ticks, ticks〉
1041	\| SWAP arg ⇒
1042	let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1043	〈ticks, ticks〉
1044	\| MOV arg ⇒
1045	let ticks ≝ ticks_of_instruction (MOV ? arg) in
1046	〈ticks, ticks〉
1047	\| MOVX arg ⇒
1048	let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1049	〈ticks, ticks〉
1050	\| SETB arg ⇒
1051	let ticks ≝ ticks_of_instruction (SETB ? arg) in
1052	〈ticks, ticks〉
1053	\| PUSH arg ⇒
1054	let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1055	〈ticks, ticks〉
1056	\| POP arg ⇒
1057	let ticks ≝ ticks_of_instruction (POP ? arg) in
1058	〈ticks, ticks〉
1059	\| XCH arg1 arg2 ⇒
1060	let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1061	〈ticks, ticks〉
1062	\| XCHD arg1 arg2 ⇒
1063	let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1064	〈ticks, ticks〉
1065	\| RET ⇒
1066	let ticks ≝ ticks_of_instruction (RET ?) in
1067	〈ticks, ticks〉
1068	\| RETI ⇒
1069	let ticks ≝ ticks_of_instruction (RETI ?) in
1070	〈ticks, ticks〉
1071	\| NOP ⇒
1072	let ticks ≝ ticks_of_instruction (NOP ?) in
1073	〈ticks, ticks〉
1074	]
1075	\| Comment comment ⇒ 〈0, 0〉
1076	\| Cost cost ⇒ 〈0, 0〉
1077	\| Jmp jmp ⇒
1078	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1079	let do_a_long ≝ policy ppc in
1080	let lookup_address ≝ sigma (lookup_labels jmp) in
1081	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1082	if sj_possible ∧ ¬ do_a_long then
1083	〈2, 2〉 (* XXX: SJMP *)
1084	else
1085	let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1086	if mj_possible ∧ ¬ do_a_long then
1087	〈2, 2〉 (* XXX: AJMP *)
1088	else
1089	〈2, 2〉 (* XXX: LJMP *)
1090	\| Call call ⇒
1091	(* XXX: collapse the branches as they are identical? *)
1092	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1093	let lookup_address ≝ sigma (lookup_labels call) in
1094	let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1095	let do_a_long ≝ policy ppc in
1096	if mj_possible ∧ ¬ do_a_long then
1097	〈2, 2〉 (* ACALL *)
1098	else
1099	〈2, 2〉 (* LCALL *)
1100	\| Mov dptr tgt ⇒ 〈2, 2〉
1101	].
1102
1103	definition ticks_of:
1104	∀p:pseudo_assembly_program.
1105	(Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1106	nat_of_bitvector … ppc < \|\snd p\| → nat × nat ≝
1107	λprogram: pseudo_assembly_program.
1108	λlookup_labels.
1109	λsigma.
1110	λpolicy.
1111	λppc: Word. λppc_ok.
1112	let pseudo ≝ \snd program in
1113	let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1114	ticks_of0 program lookup_labels sigma policy ppc fetched.
1115
1116	(*
1117	lemma blah:
1118	∀m: internal_pseudo_address_map.
1119	∀s: PseudoStatus.
1120	∀arg: Byte.
1121	∀b: bool.
1122	addressing_mode_ok m s (DIRECT arg) = true →
1123	get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1124	get_arg_8 ? s b (DIRECT arg).
1125	[2, 3: normalize % ]
1126	#m #s #arg #b #hyp
1127	whd in ⊢ (??%%)
1128	@vsplit_elim''
1129	#nu' #nl' #arg_nu_nl_eq
1130	normalize nodelta
1131	generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1132	cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1133	#get_index_v_eq
1134	normalize nodelta
1135	[2:
1136	normalize nodelta
1137	@vsplit_elim''
1138	#bit_one' #three_bits' #bit_one_three_bit_eq
1139	generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1140	normalize nodelta
1141	generalize in match (refl ? (sub_7_with_carry ? ? ?))
1142	cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1143	#Saddr #carr' #Saddr_carr_eq
1144	normalize nodelta
1145	#carr_hyp'
1146	@carr_hyp'
1147	[1:
1148	\|2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1149	generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1150	cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1151	#member_eq
1152	normalize nodelta
1153	[2: #destr destruct(destr)
1154	\|1: -carr_hyp';
1155	>arg_nu_nl_eq
1156	<(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1157	[1: >get_index_v_eq in ⊢ (??%? → ?)
1158	\|2: @le_S @le_S @le_S @le_n
1159	]
1160	cases (member (BitVector 8) ? (\fst ?) ?)
1161	[1: #destr normalize in destr; destruct(destr)
1162	\|2:
1163	]
1164	]
1165	\|3: >get_index_v_eq in ⊢ (??%?)
1166	change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1167	>(vsplit_vector_singleton … bit_one_three_bit_eq)
1168	<arg_nu_nl_eq
1169	whd in hyp:(??%?)
1170	cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1171	normalize nodelta [*: #ignore @sym_eq ]
1172	]
1173	\|
1174	].
1175	*)
1176	(*
1177	map_address0 ... (DIRECT arg) = Some .. →
1178	get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1179	get_arg_8 (internal_ram ...) (DIRECT arg)
1180
1181	((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2)
1182	then Some internal_pseudo_address_map M
1183	else None internal_pseudo_address_map )
1184	=Some internal_pseudo_address_map M')
1185
1186	axiom low_internal_ram_write_at_stack_pointer:
1187	∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1188	∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1189	get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1190	low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1191	sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1192	sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1193	bu@@bl = sigma (pbu@@pbl) →
1194	low_internal_ram T1 cm1
1195	(write_at_stack_pointer …
1196	(set_8051_sfr …
1197	(write_at_stack_pointer …
1198	(set_8051_sfr …
1199	(set_low_internal_ram … s1
1200	(low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1201	SFR_SP sp1)
1202	bl)
1203	SFR_SP sp2)
1204	bu)
1205	= low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1206	(low_internal_ram …
1207	(write_at_stack_pointer …
1208	(set_8051_sfr …
1209	(write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1210	SFR_SP sp2)
1211	pbu)).
1212
1213	lemma high_internal_ram_write_at_stack_pointer:
1214	∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1215	∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1216	get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1217	high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1218	sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1219	sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1220	bu@@bl = sigma (pbu@@pbl) →
1221	high_internal_ram T1 cm1
1222	(write_at_stack_pointer …
1223	(set_8051_sfr …
1224	(write_at_stack_pointer …
1225	(set_8051_sfr …
1226	(set_high_internal_ram … s1
1227	(high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1228	SFR_SP sp1)
1229	bl)
1230	SFR_SP sp2)
1231	bu)
1232	= high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1233	(high_internal_ram …
1234	(write_at_stack_pointer …
1235	(set_8051_sfr …
1236	(write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1237	SFR_SP sp2)
1238	pbu)).
1239	#T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1240	#get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1241	cases daemon (* XXX: !!! *)
1242	qed.
1243	*)
1244
1245	lemma snd_assembly_1_pseudoinstruction_ok:
1246	∀program: pseudo_assembly_program.
1247	∀program_length_proof: \|\snd program\| ≤ 2^16.
1248	∀sigma: Word → Word.
1249	∀policy: Word → bool.
1250	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1251	∀ppc: Word.
1252	∀ppc_in_bounds: nat_of_bitvector 16 ppc < \|\snd program\|.
1253	∀pi.
1254	∀lookup_labels.
1255	∀lookup_datalabels.
1256	let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1257	lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1258	lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1259	\fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1260	let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ((sigma ppc)) ppc lookup_datalabels pi) in
1261	sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1262	#program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1263	#lookup_labels #lookup_datalabels
1264	@pair_elim #labels #costs #create_label_cost_map_refl
1265	#lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1266	normalize nodelta
1267	generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1268	#fetch_pseudo_refl
1269	letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1270	letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1271	lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1272	@pair_elim #preamble #instr_list #program_refl
1273	lapply create_label_cost_map_refl; -create_label_cost_map_refl
1274	>program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1275	>create_label_cost_map_refl
1276	<eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1277	lapply (H ppc ppc_in_bounds) -H
1278	@pair_elim #pi' #newppc #fetch_pseudo_refl'
1279	@pair_elim #len #assembled #assembly1_refl #H
1280	cases H
1281	#encoding_check_assm #sigma_newppc_refl
1282	>fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1283	>pi_refl' in assembly1_refl; #assembly1_refl
1284	>lookup_labels_refl >lookup_datalabels_refl
1285	>program_refl normalize nodelta
1286	>assembly1_refl
1287	<sigma_newppc_refl
1288	generalize in match fetch_pseudo_refl';
1289	whd in match (fetch_pseudo_instruction ???);
1290	@pair_elim #lbl #instr #nth_refl normalize nodelta
1291	#G cases (pair_destruct_right ?????? G) %
1292	qed.
1293
1294	(* To be moved in ProofStatus *)
1295	lemma program_counter_set_program_counter:
1296	∀T.
1297	∀cm.
1298	∀s.
1299	∀x.
1300	program_counter T cm (set_program_counter T cm s x) = x.
1301	//
1302	qed.

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format