Context Navigation

AssemblyProof.ma @ 2498

Last change on this file since 2498 was 2498, checked in by mckinna, 8 years ago
Refactor: Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma Dependencies simplified.
File size: 62.0 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': costlabel_map.
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	(* XXX: if upper then the byte in the entry is the least significant byte of the address and
338	the byte in the status is the most significant, otherwise if lower then the
339	other way around
340	*)
341	definition address_entry ≝ upper_lower × Byte.
342
343	definition eq_accumulator_address_map_entry:
344	option address_entry → option address_entry → bool ≝
345	λleft.
346	λright.
347	match left with
348	[ None ⇒
349	match right with
350	[ None ⇒ true
351	\| _ ⇒ false
352	]
353	\| Some upper_lower_addr ⇒
354	let 〈upper_lower, addr〉 ≝ upper_lower_addr in
355	match right with
356	[ Some upper_lower_addr' ⇒
357	let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in
358	eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr'
359	\| _ ⇒ false
360	]
361	].
362
363	lemma eq_accumulator_address_map_entry_true_to_eq:
364	∀left: option address_entry.
365	∀right: option address_entry.
366	eq_accumulator_address_map_entry left right = true → left = right.
367	#left #right cases left cases right
368	[1:
369	#_ %
370	\|2,3:
371	* * #word normalize #absurd destruct(absurd)
372	\|4:
373	* * #word * * #word'
374	[2,3:
375	#absurd normalize in absurd; destruct(absurd)
376	]
377	normalize change with (eq_bv 8 ?? = true → ?)
378	#relevant >(eq_bv_eq … relevant) %
379	]
380	qed.
381
382	lemma eq_bv_false_to_neq:
383	∀n: nat.
384	∀left, right: BitVector n.
385	eq_bv n left right = false → left ≠ right.
386	#n #left elim left
387	[1:
388	#right >(BitVector_O … right) normalize #absurd destruct(absurd)
389	\|2:
390	#n' #hd #tl #inductive_hypothesis #right
391	cases (BitVector_Sn … right) #hd' * #tl' #right_refl
392	>right_refl normalize
393	cases hd normalize nodelta
394	cases hd' normalize nodelta
395	[2,3:
396	#_ @nmk #absurd destruct(absurd)
397	]
398	change with (eq_bv ??? = false → ?)
399	#relevant lapply (inductive_hypothesis … relevant)
400	#tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
401	#tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
402	]
403	qed.
404
405	lemma eq_accumulator_address_map_entry_false_to_neq:
406	∀left: option address_entry.
407	∀right: option address_entry.
408	eq_accumulator_address_map_entry left right = false → left ≠ right.
409	#left #right cases left cases right
410	[1:
411	normalize #absurd destruct(absurd)
412	\|2,3:
413	* * #word normalize #_ % #absurd destruct(absurd)
414	\|4:
415	* * #word * * #word' normalize
416	[2,3:
417	#_ % #absurd destruct(absurd)
418	]
419	change with (eq_bv ??? = false → ?)
420	#eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)
421	#word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm
422	#word_eq_assm @word_eq_assm destruct(address_eq_assm) %
423	]
424	qed.
425
426	(* XXX: changed this type. Bool specifies whether byte is first or second
427	component of an address, and the Word is the pseudoaddress that it
428	corresponds to. Second component is the same principle for the accumulator
429	A.
430	*)
431	definition internal_pseudo_address_map ≝
432	(* low, high, acc *)
433	(BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry).
434
435	include alias "ASM/BitVectorTrie.ma".
436
437	include "common/AssocList.ma".
438
439	axiom bvt_map2:
440	∀A, B, C: Type[0].
441	∀n: nat.
442	∀bvt_1: BitVectorTrie A n.
443	∀bvt_2: BitVectorTrie B n.
444	∀f: ∀a: option A. ∀b: option B. option C.
445	BitVectorTrie C n.
446
447	(*
448	axiom is_in_domain:
449	∀A: Type[0].
450	∀n: nat.
451	∀bvt: BitVectorTrie A n.
452	∀b: BitVector n.
453	Prop.
454
455	axiom bvt_map2_function_extensionality:
456	∀A, B, C: Type[0].
457	∀n: nat.
458	∀bvt_1: BitVectorTrie A n.
459	∀bvt_2, bvt_2': BitVectorTrie B n.
460	∀f: ∀a: option A. ∀b: option B. option C.
461	(∀addr.
462	is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr →
463	f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
464	bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
465	*)
466
467	axiom lookup_opt_bvt_map2:
468	∀A,B,C,n,map1,map2,f,addr.
469	lookup_opt … addr (bvt_map2 A B C n map1 map2 f) =
470	f (lookup_opt … addr map1) (lookup_opt … addr map2).
471
472	definition lookup_from_internal_ram:
473	∀addr: Byte.
474	∀M: internal_pseudo_address_map.
475	option address_entry ≝
476	λaddr, M.
477	let 〈low, high, accA〉 ≝ M in
478	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
479	if head' … bit_one then
480	lookup_opt … seven_bits high
481	else
482	lookup_opt … seven_bits low.
483
484	definition map_value_using_opt_address_entry:
485	(Word → Word) → Byte → option address_entry → Byte ≝
486	λsigma: Word → Word.
487	λvalue: Byte.
488	λul_addr: option address_entry.
489	match ul_addr with
490	[ None ⇒ value
491	\| Some upper_lower_word ⇒
492	let 〈upper_lower, word〉 ≝ upper_lower_word in
493	if eq_upper_lower upper_lower upper then
494	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
495	high
496	else
497	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
498	low
499	].
500
501	definition map_acc_a_using_internal_pseudo_address_map:
502	∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
503	λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).
504
505	definition map_internal_ram_address_using_pseudo_address_map:
506	∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
507	λM: internal_pseudo_address_map.
508	λsigma: Word → Word.
509	λaddress: Byte.
510	λvalue: Byte.
511	map_value_using_opt_address_entry sigma value
512	(lookup_from_internal_ram … address M ).
513
514	definition map_opt_value_using_opt_address_entry:
515	(Word → Word) → option Byte → option address_entry → option Byte ≝
516	λsigma,v,ul_addr.
517	let v ≝ match v with [ None ⇒ zero … \| Some v ⇒ v ] in
518	let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
519	if eq_bv … v' (zero …) then
520	None …
521	else
522	Some … v'.
523
524	definition internal_ram_of_pseudo_internal_ram:
525	∀sigma: Word → Word.
526	∀ram: BitVectorTrie Byte 7.
527	∀map: BitVectorTrie address_entry 7.
528	BitVectorTrie Byte 7 ≝
529	λsigma, ram, map.
530	bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
531
532	definition internal_half_pseudo_address_map_equal_up_to_address:
533	BitVectorTrie address_entry 7 → BitVectorTrie address_entry 7 → (Word → Word) →
534	BitVector 7 → Byte → Byte → Prop
535	≝
536	λM,M',sigma,addr,v,v'.
537	v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M') ∧
538	∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M'.
539
540	axiom insert_internal_ram_of_pseudo_internal_ram:
541	∀M,M',sigma,addr,v,v',ram.
542	internal_half_pseudo_address_map_equal_up_to_address M M' sigma addr v v' →
543	insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
544	= internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
545
546	definition low_internal_ram_of_pseudo_low_internal_ram:
547	∀M: internal_pseudo_address_map.
548	∀sigma: Word → Word.
549	∀ram: BitVectorTrie Byte 7.
550	BitVectorTrie Byte 7 ≝
551	λM, sigma, ram.
552	let 〈low, high, accA〉 ≝ M in
553	internal_ram_of_pseudo_internal_ram sigma ram low.
554
555	definition high_internal_ram_of_pseudo_high_internal_ram:
556	∀M: internal_pseudo_address_map.
557	∀sigma: Word → Word.
558	∀ram: BitVectorTrie Byte 7.
559	BitVectorTrie Byte 7 ≝
560	λM, sigma, ram.
561	let 〈low, high, accA〉 ≝ M in
562	internal_ram_of_pseudo_internal_ram sigma ram high.
563
564	(*
565	axiom low_internal_ram_of_pseudo_internal_ram_hit:
566	∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
567	lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉 →
568	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
569	let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
570	let bl ≝ lookup ? 7 addr ram (zero 8) in
571	let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
572	let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
573	if eq_upper_lower upper_lower upper then
574	(pbl = higher) ∧ (bl = phigher)
575	else
576	(pbl = lower) ∧ (bl = plower).
577	*)
578
579	(* changed from add to sub *)
580	axiom low_internal_ram_of_pseudo_internal_ram_miss:
581	∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
582	let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
583	lookup_opt … addr (\fst (\fst M)) = None … →
584	lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).
585
586	definition exists:
587	∀A: Type[0].
588	∀n: nat.
589	∀v: BitVector n.
590	∀bvt: BitVectorTrie A n.
591	bool ≝
592	λA, n, v, bvt.
593	match lookup_opt … v bvt with
594	[ None ⇒ false
595	\| _ ⇒ true
596	].
597
598	definition data_or_address ≝
599	λT.
600	λM: internal_pseudo_address_map.
601	λcm.
602	λs: PreStatus T cm.
603	λaddr: addressing_mode.
604	let 〈low, high, accA〉 ≝ M in
605	match addr return λx. option (option address_entry) with
606	[ DIRECT d ⇒
607	let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
608	match head' … hd with
609	[ true ⇒
610	if eq_bv … d (bitvector_of_nat … 224) then
611	Some … accA
612	else
613	Some … (None …)
614	\| false ⇒ Some … (lookup_opt … seven_bits low)
615	]
616	\| INDIRECT i ⇒
617	let d ≝ get_register … s [[false;false;i]] in
618	let address ≝ bit_address_of_register … s [[false;false;i]] in
619	if ¬exists … address low then
620	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
621	if head' … 0 bit_one then
622	Some … (lookup_opt … seven_bits high)
623	else
624	Some … (lookup_opt … seven_bits low)
625	else
626	None ?
627	\| EXT_INDIRECT e ⇒
628	let address ≝ bit_address_of_register … s [[false;false;e]] in
629	if ¬exists … address low then
630	Some … (None …)
631	else
632	None ?
633	\| REGISTER r ⇒
634	let address ≝ bit_address_of_register … s r in
635	Some … (lookup_opt … address low)
636	\| ACC_A ⇒ Some … accA
637	\| ACC_B ⇒ Some … (None …)
638	\| DPTR ⇒ Some … (None …)
639	\| DATA _ ⇒ Some … (None …)
640	\| DATA16 _ ⇒ Some … (None …)
641	\| ACC_DPTR ⇒ Some … (None …)
642	\| ACC_PC ⇒ Some … (None …)
643	\| EXT_INDIRECT_DPTR ⇒ Some … (None …)
644	\| INDIRECT_DPTR ⇒ Some … (None …)
645	\| CARRY ⇒ Some … (None …)
646	\| BIT_ADDR b ⇒
647	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
648	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
649	if head' bool 0 bit_one then
650	if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
651	Some … accA
652	else
653	Some … (None …)
654	else
655	let address' ≝ [[true; false; false]]@@four_bits in
656	Some … (lookup_opt … address' low)
657	\| N_BIT_ADDR b ⇒
658	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
659	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
660	if head' bool 0 bit_one then
661	if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
662	Some … accA
663	else
664	Some … (None …)
665	else
666	let address' ≝ [[true; false; false]]@@four_bits in
667	Some … (lookup_opt … address' low)
668	\| RELATIVE _ ⇒ Some … (None …)
669	\| ADDR11 _ ⇒ Some … (None …)
670	\| ADDR16 _ ⇒ Some … (None …)
671	].
672
673	definition assert_data ≝
674	λT.
675	λM: internal_pseudo_address_map.
676	λcm.
677	λs: PreStatus T cm.
678	λaddr: addressing_mode.
679	match data_or_address T M cm s addr with
680	[ None ⇒ false
681	\| Some s ⇒
682	match s with
683	[ None ⇒ true
684	\| _ ⇒ false
685	]
686	].
687
688	definition insert_into_internal_ram:
689	∀addr: Byte.
690	∀v: address_entry.
691	∀M: internal_pseudo_address_map.
692	internal_pseudo_address_map ≝
693	λaddr, v, M.
694	let 〈low, high, accA〉 ≝ M in
695	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
696	if head' … bit_one then
697	〈low, insert … seven_bits v high, accA〉
698	else
699	〈insert … seven_bits v low, high, accA〉.
700
701	axiom delete:
702	∀A: Type[0].
703	∀n: nat.
704	∀b: BitVector n.
705	BitVectorTrie A n → BitVectorTrie A n.
706
707	definition delete_from_internal_ram:
708	∀addr: Byte.
709	∀M: internal_pseudo_address_map.
710	internal_pseudo_address_map ≝
711	λaddr, M.
712	let 〈low, high, accA〉 ≝ M in
713	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
714	if head' … bit_one then
715	〈low,delete … seven_bits high, accA〉
716	else
717	〈delete … seven_bits low, high, accA〉.
718
719	definition overwrite_or_delete_from_internal_ram:
720	∀addr: Byte.
721	∀v: option address_entry.
722	∀M: internal_pseudo_address_map.
723	internal_pseudo_address_map ≝
724	λaddr, v, M.
725	match v with
726	[ None ⇒ delete_from_internal_ram addr M
727	\| Some v' ⇒ insert_into_internal_ram addr v' M
728	].
729
730	definition next_internal_pseudo_address_map0 ≝
731	λT.
732	λcm:T.
733	λaddr_of: Identifier → PreStatus T cm → Word.
734	λfetched.
735	λM: internal_pseudo_address_map.
736	λs: PreStatus T cm.
737	let 〈low, high, accA〉 ≝ M in
738	match fetched with
739	[ Comment _ ⇒ Some ? M
740	\| Cost _ ⇒ Some … M
741	\| Jmp _ ⇒ Some … M
742	\| Call a ⇒
743	let a' ≝ addr_of a s in
744	let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
745	Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
746	(insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
747	\| Mov _ _ ⇒ Some … M
748	\| Instruction instr ⇒
749	match instr return λx. option internal_pseudo_address_map with
750	[ ADD addr1 addr2 ⇒
751	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
752	Some ? M
753	else
754	None ?
755	\| ADDC addr1 addr2 ⇒
756	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
757	Some ? M
758	else
759	None ?
760	\| SUBB addr1 addr2 ⇒
761	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
762	Some ? M
763	else
764	None ?
765	\| INC addr1 ⇒
766	if assert_data T M ? s addr1 then
767	Some ? M
768	else
769	None ?
770	\| DEC addr1 ⇒
771	if assert_data T M … s addr1 then
772	Some ? M
773	else
774	None ?
775	\| MUL addr1 addr2 ⇒
776	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
777	Some ? M
778	else
779	None ?
780	\| DIV addr1 addr2 ⇒
781	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
782	Some ? M
783	else
784	None ?
785	\| DA addr1 ⇒
786	if assert_data T M … s addr1 then
787	Some ? M
788	else
789	None ?
790	\| JC addr1 ⇒ Some ? M
791	\| JNC addr1 ⇒ Some ? M
792	\| JB addr1 addr2 ⇒ Some ? M
793	\| JNB addr1 addr2 ⇒ Some ? M
794	\| JBC addr1 addr2 ⇒ Some ? M
795	\| JZ addr1 ⇒ Some ? M
796	\| JNZ addr1 ⇒ Some ? M
797	\| CJNE addr1 addr2 ⇒
798	match addr1 with
799	[ inl l ⇒
800	let 〈left, right〉 ≝ l in
801	if assert_data T M … s left ∧ assert_data T M … s right then
802	Some ? M
803	else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
804	Some ? M
805	else
806	None ?
807	\| inr r ⇒
808	let 〈left, right〉 ≝ r in
809	if assert_data T M … s left ∧ assert_data T M … s right then
810	Some ? M
811	else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
812	Some ? M
813	else
814	None ?
815	]
816	\| DJNZ addr1 addr2 ⇒
817	if assert_data T M … s addr1 then
818	Some ? M
819	else
820	None ?
821	\| CLR addr1 ⇒
822	if assert_data T M … s addr1 then
823	Some ? M
824	else
825	None ?
826	\| CPL addr1 ⇒
827	if assert_data T M … s addr1 then
828	Some ? M
829	else
830	None ?
831	\| RL addr1 ⇒
832	if assert_data T M … s addr1 then
833	Some ? M
834	else
835	None ?
836	\| RLC addr1 ⇒
837	if assert_data T M … s addr1 then
838	Some ? M
839	else
840	None ?
841	\| RR addr1 ⇒
842	if assert_data T M … s addr1 then
843	Some ? M
844	else
845	None ?
846	\| RRC addr1 ⇒
847	if assert_data T M … s addr1 then
848	Some ? M
849	else
850	None ?
851	\| SWAP addr1 ⇒
852	if assert_data T M … s addr1 then
853	Some ? M
854	else
855	None ?
856	\| SETB addr1 ⇒
857	if assert_data T M … s addr1 then
858	Some ? M
859	else
860	None ?
861	(* XXX: need to track addresses pushed and popped off the stack? *)
862	\| PUSH addr1 ⇒
863	match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
864	[ DIRECT d ⇒ λproof.
865	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
866	if head' … bit_one then
867	if eq_bv … seven_bits (bitvector_of_nat … 224) then
868	Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
869	else
870	Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
871	else
872	Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
873	\| _ ⇒ λother: False. ⊥
874	] (subaddressing_modein … addr1)
875	\| POP addr1 ⇒
876	let sp ≝ get_8051_sfr ?? s SFR_SP in
877	match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
878	[ DIRECT d ⇒ λproof.
879	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
880	if head' … bit_one then
881	if eq_bv … d (bitvector_of_nat … 224) then
882	Some … 〈low, high, lookup_from_internal_ram … sp M〉
883	else
884	match lookup_from_internal_ram sp M with
885	[ None ⇒ Some ? M
886	\| _ ⇒ None ?
887	]
888	else
889	Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
890	\| _ ⇒ λother: False. ⊥
891	] (subaddressing_modein … addr1)
892	\| XCH addr1 addr2 ⇒
893	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
894	Some ? M
895	else
896	None ?
897	\| XCHD addr1 addr2 ⇒
898	if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
899	Some ? M
900	else
901	None ?
902	\| RET ⇒
903	let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
904	let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
905	match lookup_from_internal_ram sp_minus_1 M with
906	[ None ⇒ None …
907	\| Some low_addr_high ⇒
908	match lookup_from_internal_ram sp_minus_2 M with
909	[ None ⇒ None …
910	\| Some high_addr_low ⇒
911	let 〈low, addr_high〉 ≝ low_addr_high in
912	let 〈high, addr_low〉 ≝ high_addr_low in
913	let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
914	let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
915	if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
916	Some ? M
917	else
918	None ?
919	]
920	]
921	\| RETI ⇒
922	let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
923	let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
924	match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
925	[ None ⇒ None …
926	\| Some low_addr_high ⇒
927	match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
928	[ None ⇒ None …
929	\| Some high_addr_low ⇒
930	let 〈low, addr_high〉 ≝ low_addr_high in
931	let 〈high, addr_low〉 ≝ high_addr_low in
932	let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
933	let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
934	if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
935	Some ? M
936	else
937	None ?
938	]
939	]
940	\| NOP ⇒ Some … M
941	\| MOVX addr1 ⇒
942	match addr1 with
943	[ inl l ⇒
944	Some ? 〈low, high, None …〉
945	\| inr r ⇒
946	let 〈others, acc_a〉 ≝ r in
947	if assert_data T M … s acc_a then
948	Some ? M
949	else
950	None ?
951	]
952	\| XRL addr1 ⇒
953	match addr1 with
954	[ inl l ⇒
955	let 〈acc_a, others〉 ≝ l in
956	let acc_a_ok ≝ assert_data T M … s acc_a in
957	let others_ok ≝ assert_data T M … s others in
958	if acc_a_ok ∧ others_ok then
959	Some ? M
960	else
961	None ?
962	\| inr r ⇒
963	let 〈direct, others〉 ≝ r in
964	let direct_ok ≝ assert_data T M … s direct in
965	let others_ok ≝ assert_data T M … s others in
966	if direct_ok ∧ others_ok then
967	Some ? M
968	else
969	None ?
970	]
971	\| ORL addr1 ⇒
972	match addr1 with
973	[ inl l ⇒
974	match l with
975	[ inl l ⇒
976	let 〈acc_a, others〉 ≝ l in
977	let acc_a_ok ≝ assert_data T M … s acc_a in
978	let others_ok ≝ assert_data T M … s others in
979	if acc_a_ok ∧ others_ok then
980	Some ? M
981	else
982	None ?
983	\| inr r ⇒
984	let 〈direct, others〉 ≝ r in
985	let direct_ok ≝ assert_data T M … s direct in
986	let others_ok ≝ assert_data T M … s others in
987	if direct_ok ∧ others_ok then
988	Some ? M
989	else
990	None ?
991	]
992	\| inr r ⇒
993	let 〈carry, others〉 ≝ r in
994	let carry_ok ≝ assert_data T M … s carry in
995	let others_ok ≝ assert_data T M … s others in
996	if carry_ok ∧ others_ok then
997	Some ? M
998	else
999	None ?
1000	]
1001	\| ANL addr1 ⇒
1002	match addr1 with
1003	[ inl l ⇒
1004	match l with
1005	[ inl l ⇒
1006	let 〈acc_a, others〉 ≝ l in
1007	let acc_a_ok ≝ assert_data T M … s acc_a in
1008	let others_ok ≝ assert_data T M … s others in
1009	if acc_a_ok ∧ others_ok then
1010	Some ? M
1011	else
1012	None ?
1013	\| inr r ⇒
1014	let 〈direct, others〉 ≝ r in
1015	let direct_ok ≝ assert_data T M … s direct in
1016	let others_ok ≝ assert_data T M … s others in
1017	if direct_ok ∧ others_ok then
1018	Some ? M
1019	else
1020	None ?
1021	]
1022	\| inr r ⇒
1023	let 〈carry, others〉 ≝ r in
1024	let carry_ok ≝ assert_data T M … s carry in
1025	let others_ok ≝ assert_data T M … s others in
1026	if carry_ok ∧ others_ok then
1027	Some ? M
1028	else
1029	None ?
1030	]
1031	\| MOV addr1 ⇒
1032	(* XXX: wrong *)
1033	match addr1 with
1034	[ inl l ⇒
1035	match l with
1036	[ inl l' ⇒
1037	match l' with
1038	[ inl l'' ⇒
1039	match l'' with
1040	[ inl l''' ⇒
1041	match l''' with
1042	[ inl l'''' ⇒
1043	let 〈acc_a, others〉 ≝ l'''' in
1044	match data_or_address T M … s others with
1045	[ None ⇒ None ?
1046	\| Some s ⇒
1047	Some … 〈low, high, s〉
1048	]
1049	\| inr r ⇒
1050	let 〈others, others'〉 ≝ r in
1051	let address ≝
1052	match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
1053	[ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
1054	\| INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
1055	\| _ ⇒ λother: False. ⊥
1056	] (subaddressing_modein … others)
1057	in
1058	match data_or_address T M … s others' with
1059	[ None ⇒ None ?
1060	\| Some s ⇒
1061	Some … (overwrite_or_delete_from_internal_ram address s M)
1062	]
1063	]
1064	\| inr r ⇒
1065	let 〈direct', others〉 ≝ r in
1066	match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
1067	[ DIRECT d ⇒ λproof.
1068	match data_or_address T M … s others with
1069	[ None ⇒ None ?
1070	\| Some s' ⇒
1071	let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
1072	if head' … bit_one then
1073	if eq_bv … d (bitvector_of_nat … 224) then
1074	Some … 〈low, high, s'〉
1075	else
1076	match s' with
1077	[ None ⇒ Some ? M
1078	\| Some s'' ⇒ None ?
1079	]
1080	else
1081	Some … (overwrite_or_delete_from_internal_ram d s' M)
1082	]
1083	\| _ ⇒ λother: False. ⊥
1084	] (subaddressing_modein … direct')
1085	]
1086	\| inr r ⇒ Some … M
1087	]
1088	\| inr r ⇒
1089	let 〈carry, bit_addr〉 ≝ r in
1090	if assert_data T M … s bit_addr then
1091	Some ? M
1092	else
1093	None ?
1094	]
1095	\| inr r ⇒
1096	let 〈bit_addr, carry〉 ≝ r in
1097	if assert_data T M … s bit_addr then
1098	Some ? M
1099	else
1100	None ?
1101	]
1102	]
1103	].
1104	cases other
1105	qed.
1106
1107	definition next_internal_pseudo_address_map ≝
1108	λM:internal_pseudo_address_map.
1109	λcm.
1110	λaddr_of.
1111	λs:PseudoStatus cm.
1112	λppc_ok.
1113	next_internal_pseudo_address_map0 ? cm addr_of
1114	(\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1115
1116	definition code_memory_of_pseudo_assembly_program:
1117	∀pap:pseudo_assembly_program.
1118	(Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1119	λpap.
1120	λsigma.
1121	λpolicy.
1122	let p ≝ pi1 … (assembly pap sigma policy) in
1123	load_code_memory (\fst p).
1124
1125	definition sfr_8051_of_pseudo_sfr_8051 ≝
1126	λM: internal_pseudo_address_map.
1127	λsfrs: Vector Byte 19.
1128	λsigma: Word → Word.
1129	match \snd M with
1130	[ None ⇒ sfrs
1131	\| Some upper_lower_address ⇒
1132	let index ≝ sfr_8051_index SFR_ACC_A in
1133	let acc_a ≝ get_index_v … sfrs index ? in
1134	let 〈upper_lower, address〉 ≝ upper_lower_address in
1135	if eq_upper_lower upper_lower upper then
1136	let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
1137	set_index Byte 19 sfrs index high ?
1138	else
1139	let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
1140	set_index Byte 19 sfrs index low ?
1141	].
1142	//
1143	qed.
1144
1145	definition status_of_pseudo_status:
1146	internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1147	∀sigma: Word → Word. ∀policy: Word → bool.
1148	Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1149	λM.
1150	λpap.
1151	λps.
1152	λsigma.
1153	λpolicy.
1154	let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1155	let pc ≝ sigma (program_counter … ps) in
1156	let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
1157	let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
1158	mk_PreStatus (BitVectorTrie Byte 16)
1159	cm
1160	lir
1161	hir
1162	(external_ram … ps)
1163	pc
1164	(sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
1165	(special_function_registers_8052 … ps)
1166	(p1_latch … ps)
1167	(p3_latch … ps)
1168	(clock … ps).
1169
1170	(*
1171	definition write_at_stack_pointer':
1172	∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1173	λM: Type[0].
1174	λs: PreStatus M.
1175	λv: Byte.
1176	let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1177	let bit_zero ≝ get_index_v… nu O ? in
1178	let bit_1 ≝ get_index_v… nu 1 ? in
1179	let bit_2 ≝ get_index_v… nu 2 ? in
1180	let bit_3 ≝ get_index_v… nu 3 ? in
1181	if bit_zero then
1182	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1183	v (low_internal_ram ? s) in
1184	set_low_internal_ram ? s memory
1185	else
1186	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1187	v (high_internal_ram ? s) in
1188	set_high_internal_ram ? s memory.
1189	[ cases l0 %
1190	\|2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1191	qed.
1192
1193	definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1194	Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1195	≝
1196	λticks_of.
1197	λs.
1198	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1199	let ticks ≝ ticks_of (program_counter ? s) in
1200	let s ≝ set_clock ? s (clock ? s + ticks) in
1201	let s ≝ set_program_counter ? s pc in
1202	match instr with
1203	[ Instruction instr ⇒
1204	execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1205	\| Comment cmt ⇒ s
1206	\| Cost cst ⇒ s
1207	\| Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1208	\| Call call ⇒
1209	let a ≝ address_of_word_labels s call in
1210	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1211	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1212	let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1213	let s ≝ write_at_stack_pointer' ? s pc_bl in
1214	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1215	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1216	let s ≝ write_at_stack_pointer' ? s pc_bu in
1217	set_program_counter ? s a
1218	\| Mov dptr ident ⇒
1219	set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1220	].
1221	[
1222	\|2,3,4: %
1223	\| <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1224	\|
1225	\| %
1226	]
1227	cases not_implemented
1228	qed.
1229	*)
1230
1231	(*
1232	lemma execute_code_memory_unchanged:
1233	∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1234	#ticks #ps whd in ⊢ (??? (??%))
1235	cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1236	(program_counter pseudo_assembly_program ps)) #instr #pc
1237	whd in ⊢ (??? (??%)) cases instr
1238	[ #pre cases pre
1239	[ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1240	cases (vsplit ????) #z1 #z2 %
1241	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1242	cases (vsplit ????) #z1 #z2 %
1243	\| #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1244	cases (vsplit ????) #z1 #z2 %
1245	\| #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1246	[ #x1 whd in ⊢ (??? (??%))
1247	\| *: cases not_implemented
1248	]
1249	\| #comment %
1250	\| #cost %
1251	\| #label %
1252	\| #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1253	cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1254	whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1255	whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1256	(* CSC: ??? *)
1257	\| #dptr #label (* CSC: ??? *)
1258	]
1259	cases not_implemented
1260	qed.
1261	*)
1262
1263	(* XXX: check values returned for conditional jumps below! They are wrong,
1264	find correct values *)
1265	definition ticks_of0:
1266	∀p:pseudo_assembly_program.
1267	(Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1268	λprogram: pseudo_assembly_program.
1269	λlookup_labels: Identifier → Word.
1270	λsigma.
1271	λpolicy.
1272	λppc: Word.
1273	λfetched.
1274	match fetched with
1275	[ Instruction instr ⇒
1276	match instr with
1277	[ JC lbl ⇒
1278	let lookup_address ≝ sigma (lookup_labels lbl) in
1279	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1280	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1281	if sj_possible then
1282	〈2, 2〉
1283	else
1284	〈4, 4〉
1285	\| JNC lbl ⇒
1286	let lookup_address ≝ sigma (lookup_labels lbl) in
1287	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1288	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1289	if sj_possible then
1290	〈2, 2〉
1291	else
1292	〈4, 4〉
1293	\| JB bit lbl ⇒
1294	let lookup_address ≝ sigma (lookup_labels lbl) in
1295	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1296	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1297	if sj_possible then
1298	〈2, 2〉
1299	else
1300	〈4, 4〉
1301	\| JNB bit lbl ⇒
1302	let lookup_address ≝ sigma (lookup_labels lbl) in
1303	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1304	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1305	if sj_possible then
1306	〈2, 2〉
1307	else
1308	〈4, 4〉
1309	\| JBC bit lbl ⇒
1310	let lookup_address ≝ sigma (lookup_labels lbl) in
1311	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1312	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1313	if sj_possible then
1314	〈2, 2〉
1315	else
1316	〈4, 4〉
1317	\| JZ lbl ⇒
1318	let lookup_address ≝ sigma (lookup_labels lbl) in
1319	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1320	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1321	if sj_possible then
1322	〈2, 2〉
1323	else
1324	〈4, 4〉
1325	\| JNZ lbl ⇒
1326	let lookup_address ≝ sigma (lookup_labels lbl) in
1327	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1328	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1329	if sj_possible then
1330	〈2, 2〉
1331	else
1332	〈4, 4〉
1333	\| CJNE arg lbl ⇒
1334	let lookup_address ≝ sigma (lookup_labels lbl) in
1335	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1336	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1337	if sj_possible then
1338	〈2, 2〉
1339	else
1340	〈4, 4〉
1341	\| DJNZ arg lbl ⇒
1342	let lookup_address ≝ sigma (lookup_labels lbl) in
1343	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1344	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1345	if sj_possible then
1346	〈2, 2〉
1347	else
1348	〈4, 4〉
1349	\| ADD arg1 arg2 ⇒
1350	let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1351	〈ticks, ticks〉
1352	\| ADDC arg1 arg2 ⇒
1353	let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1354	〈ticks, ticks〉
1355	\| SUBB arg1 arg2 ⇒
1356	let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1357	〈ticks, ticks〉
1358	\| INC arg ⇒
1359	let ticks ≝ ticks_of_instruction (INC ? arg) in
1360	〈ticks, ticks〉
1361	\| DEC arg ⇒
1362	let ticks ≝ ticks_of_instruction (DEC ? arg) in
1363	〈ticks, ticks〉
1364	\| MUL arg1 arg2 ⇒
1365	let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1366	〈ticks, ticks〉
1367	\| DIV arg1 arg2 ⇒
1368	let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1369	〈ticks, ticks〉
1370	\| DA arg ⇒
1371	let ticks ≝ ticks_of_instruction (DA ? arg) in
1372	〈ticks, ticks〉
1373	\| ANL arg ⇒
1374	let ticks ≝ ticks_of_instruction (ANL ? arg) in
1375	〈ticks, ticks〉
1376	\| ORL arg ⇒
1377	let ticks ≝ ticks_of_instruction (ORL ? arg) in
1378	〈ticks, ticks〉
1379	\| XRL arg ⇒
1380	let ticks ≝ ticks_of_instruction (XRL ? arg) in
1381	〈ticks, ticks〉
1382	\| CLR arg ⇒
1383	let ticks ≝ ticks_of_instruction (CLR ? arg) in
1384	〈ticks, ticks〉
1385	\| CPL arg ⇒
1386	let ticks ≝ ticks_of_instruction (CPL ? arg) in
1387	〈ticks, ticks〉
1388	\| RL arg ⇒
1389	let ticks ≝ ticks_of_instruction (RL ? arg) in
1390	〈ticks, ticks〉
1391	\| RLC arg ⇒
1392	let ticks ≝ ticks_of_instruction (RLC ? arg) in
1393	〈ticks, ticks〉
1394	\| RR arg ⇒
1395	let ticks ≝ ticks_of_instruction (RR ? arg) in
1396	〈ticks, ticks〉
1397	\| RRC arg ⇒
1398	let ticks ≝ ticks_of_instruction (RRC ? arg) in
1399	〈ticks, ticks〉
1400	\| SWAP arg ⇒
1401	let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1402	〈ticks, ticks〉
1403	\| MOV arg ⇒
1404	let ticks ≝ ticks_of_instruction (MOV ? arg) in
1405	〈ticks, ticks〉
1406	\| MOVX arg ⇒
1407	let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1408	〈ticks, ticks〉
1409	\| SETB arg ⇒
1410	let ticks ≝ ticks_of_instruction (SETB ? arg) in
1411	〈ticks, ticks〉
1412	\| PUSH arg ⇒
1413	let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1414	〈ticks, ticks〉
1415	\| POP arg ⇒
1416	let ticks ≝ ticks_of_instruction (POP ? arg) in
1417	〈ticks, ticks〉
1418	\| XCH arg1 arg2 ⇒
1419	let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1420	〈ticks, ticks〉
1421	\| XCHD arg1 arg2 ⇒
1422	let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1423	〈ticks, ticks〉
1424	\| RET ⇒
1425	let ticks ≝ ticks_of_instruction (RET ?) in
1426	〈ticks, ticks〉
1427	\| RETI ⇒
1428	let ticks ≝ ticks_of_instruction (RETI ?) in
1429	〈ticks, ticks〉
1430	\| NOP ⇒
1431	let ticks ≝ ticks_of_instruction (NOP ?) in
1432	〈ticks, ticks〉
1433	]
1434	\| Comment comment ⇒ 〈0, 0〉
1435	\| Cost cost ⇒ 〈0, 0〉
1436	\| Jmp jmp ⇒
1437	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1438	let do_a_long ≝ policy ppc in
1439	let lookup_address ≝ sigma (lookup_labels jmp) in
1440	let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1441	if sj_possible ∧ ¬ do_a_long then
1442	〈2, 2〉 (* XXX: SJMP *)
1443	else
1444	let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1445	if mj_possible ∧ ¬ do_a_long then
1446	〈2, 2〉 (* XXX: AJMP *)
1447	else
1448	〈2, 2〉 (* XXX: LJMP *)
1449	\| Call call ⇒
1450	(* XXX: collapse the branches as they are identical? *)
1451	let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1452	let lookup_address ≝ sigma (lookup_labels call) in
1453	let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1454	let do_a_long ≝ policy ppc in
1455	if mj_possible ∧ ¬ do_a_long then
1456	〈2, 2〉 (* ACALL *)
1457	else
1458	〈2, 2〉 (* LCALL *)
1459	\| Mov dptr tgt ⇒ 〈2, 2〉
1460	].
1461
1462	definition ticks_of:
1463	∀p:pseudo_assembly_program.
1464	(Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1465	nat_of_bitvector … ppc < \|\snd p\| → nat × nat ≝
1466	λprogram: pseudo_assembly_program.
1467	λlookup_labels.
1468	λsigma.
1469	λpolicy.
1470	λppc: Word. λppc_ok.
1471	let pseudo ≝ \snd program in
1472	let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1473	ticks_of0 program lookup_labels sigma policy ppc fetched.
1474
1475	(*
1476	lemma blah:
1477	∀m: internal_pseudo_address_map.
1478	∀s: PseudoStatus.
1479	∀arg: Byte.
1480	∀b: bool.
1481	assert_data m s (DIRECT arg) = true →
1482	get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1483	get_arg_8 ? s b (DIRECT arg).
1484	[2, 3: normalize % ]
1485	#m #s #arg #b #hyp
1486	whd in ⊢ (??%%)
1487	@vsplit_elim''
1488	#nu' #nl' #arg_nu_nl_eq
1489	normalize nodelta
1490	generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1491	cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1492	#get_index_v_eq
1493	normalize nodelta
1494	[2:
1495	normalize nodelta
1496	@vsplit_elim''
1497	#bit_one' #three_bits' #bit_one_three_bit_eq
1498	generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1499	normalize nodelta
1500	generalize in match (refl ? (sub_7_with_carry ? ? ?))
1501	cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1502	#Saddr #carr' #Saddr_carr_eq
1503	normalize nodelta
1504	#carr_hyp'
1505	@carr_hyp'
1506	[1:
1507	\|2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1508	generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1509	cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1510	#member_eq
1511	normalize nodelta
1512	[2: #destr destruct(destr)
1513	\|1: -carr_hyp';
1514	>arg_nu_nl_eq
1515	<(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1516	[1: >get_index_v_eq in ⊢ (??%? → ?)
1517	\|2: @le_S @le_S @le_S @le_n
1518	]
1519	cases (member (BitVector 8) ? (\fst ?) ?)
1520	[1: #destr normalize in destr; destruct(destr)
1521	\|2:
1522	]
1523	]
1524	\|3: >get_index_v_eq in ⊢ (??%?)
1525	change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1526	>(vsplit_vector_singleton … bit_one_three_bit_eq)
1527	<arg_nu_nl_eq
1528	whd in hyp:(??%?)
1529	cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1530	normalize nodelta [*: #ignore @sym_eq ]
1531	]
1532	\|
1533	].
1534	*)
1535	(*
1536	map_address0 ... (DIRECT arg) = Some .. →
1537	get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1538	get_arg_8 (internal_ram ...) (DIRECT arg)
1539
1540	((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2)
1541	then Some internal_pseudo_address_map M
1542	else None internal_pseudo_address_map )
1543	=Some internal_pseudo_address_map M')
1544
1545	axiom low_internal_ram_write_at_stack_pointer:
1546	∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1547	∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1548	get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1549	low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1550	sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1551	sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1552	bu@@bl = sigma (pbu@@pbl) →
1553	low_internal_ram T1 cm1
1554	(write_at_stack_pointer …
1555	(set_8051_sfr …
1556	(write_at_stack_pointer …
1557	(set_8051_sfr …
1558	(set_low_internal_ram … s1
1559	(low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1560	SFR_SP sp1)
1561	bl)
1562	SFR_SP sp2)
1563	bu)
1564	= low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1565	(low_internal_ram …
1566	(write_at_stack_pointer …
1567	(set_8051_sfr …
1568	(write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1569	SFR_SP sp2)
1570	pbu)).
1571
1572	lemma high_internal_ram_write_at_stack_pointer:
1573	∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1574	∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1575	get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1576	high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1577	sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1578	sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1579	bu@@bl = sigma (pbu@@pbl) →
1580	high_internal_ram T1 cm1
1581	(write_at_stack_pointer …
1582	(set_8051_sfr …
1583	(write_at_stack_pointer …
1584	(set_8051_sfr …
1585	(set_high_internal_ram … s1
1586	(high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1587	SFR_SP sp1)
1588	bl)
1589	SFR_SP sp2)
1590	bu)
1591	= high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1592	(high_internal_ram …
1593	(write_at_stack_pointer …
1594	(set_8051_sfr …
1595	(write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1596	SFR_SP sp2)
1597	pbu)).
1598	#T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1599	#get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1600	cases daemon (* XXX: !!! *)
1601	qed.
1602	*)
1603
1604	lemma snd_assembly_1_pseudoinstruction_ok:
1605	∀program: pseudo_assembly_program.
1606	∀program_length_proof: \|\snd program\| ≤ 2^16.
1607	∀sigma: Word → Word.
1608	∀policy: Word → bool.
1609	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1610	∀ppc: Word.
1611	∀ppc_in_bounds: nat_of_bitvector 16 ppc < \|\snd program\|.
1612	∀pi.
1613	∀lookup_labels.
1614	∀lookup_datalabels.
1615	let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1616	lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1617	lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1618	\fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1619	let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ((sigma ppc)) ppc lookup_datalabels pi) in
1620	sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1621	#program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1622	#lookup_labels #lookup_datalabels
1623	@pair_elim #labels #costs #create_label_cost_map_refl
1624	#lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1625	normalize nodelta
1626	generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1627	#fetch_pseudo_refl
1628	letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1629	letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1630	lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1631	@pair_elim #preamble #instr_list #program_refl
1632	lapply create_label_cost_map_refl; -create_label_cost_map_refl
1633	>program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1634	>create_label_cost_map_refl
1635	<eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1636	lapply (H ppc ppc_in_bounds) -H
1637	@pair_elim #pi' #newppc #fetch_pseudo_refl'
1638	@pair_elim #len #assembled #assembly1_refl #H
1639	cases H
1640	#encoding_check_assm #sigma_newppc_refl
1641	>fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1642	>pi_refl' in assembly1_refl; #assembly1_refl
1643	>lookup_labels_refl >lookup_datalabels_refl
1644	>program_refl normalize nodelta
1645	>assembly1_refl
1646	<sigma_newppc_refl
1647	generalize in match fetch_pseudo_refl';
1648	whd in match (fetch_pseudo_instruction ???);
1649	@pair_elim #lbl #instr #nth_refl normalize nodelta
1650	#G cases (pair_destruct_right ?????? G) %
1651	qed.
1652
1653	(* To be moved in ProofStatus *)
1654	lemma program_counter_set_program_counter:
1655	∀T.
1656	∀cm.
1657	∀s.
1658	∀x.
1659	program_counter T cm (set_program_counter T cm s x) = x.
1660	//
1661	qed.

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

Download in other formats:

Original Format