Context Navigation

Test.ma @ 2273

Last change on this file since 2273 was 2273, checked in by sacerdot, 9 years ago
lemmas moved from all files to Test.ma most of the lemmas in Test.ma repaired. A few are commented out. Several needs to be slightly generalized.
File size: 80.4 KB

Line
1	include "ASM/Assembly.ma".
2	include "ASM/Interpret.ma".
3	include "ASM/StatusProofs.ma".
4	include alias "arithmetics/nat.ma".
5	include "ASM/AssemblyProof.ma".
6
7	lemma let_pair_in_status_of_pseudo_status:
8	∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
9	c = c' →
10	(∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
11	(let 〈left, right〉 ≝ c' in s' left right c') =
12	status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
13	#A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
14	qed.
15
16	lemma let_pair_as_in_status_of_pseudo_status:
17	∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
18	c = c' →
19	(∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →
20	(let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
21	status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
22	#A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
23	destruct(destruct_refl) /2/
24	qed.
25
26	lemma if_then_else_status_of_pseudo_status:
27	∀M: internal_pseudo_address_map.
28	∀cm: pseudo_assembly_program.
29	∀sigma: Word → Word.
30	∀policy: Word → bool.
31	∀s, s', s'', s'''.
32	∀t, t': bool.
33	t = t' →
34	status_of_pseudo_status M cm s sigma policy = s' →
35	status_of_pseudo_status M cm s'' sigma policy = s''' →
36	if t then
37	s'
38	else
39	s''' =
40	status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
41	#M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
42	>t_refl normalize nodelta >s_refl cases t' normalize nodelta //
43	qed.
44
45	lemma set_program_counter_status_of_pseudo_status:
46	∀M.
47	∀cm.
48	∀sigma.
49	∀policy.
50	∀s, s'.
51	∀new_ppc, new_ppc'.
52	sigma new_ppc = new_ppc' →
53	status_of_pseudo_status M cm s sigma policy = s' →
54	set_program_counter (BitVectorTrie Byte 16)
55	(code_memory_of_pseudo_assembly_program cm sigma policy)
56	s' new_ppc' =
57	status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
58	#M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
59	#new_ppc_refl #s_refl <new_ppc_refl <s_refl //
60	qed.
61
62	lemma set_p1_latch_status_of_pseudo_status:
63	∀M.
64	∀code_memory.
65	∀sigma.
66	∀policy.
67	∀s,s'.
68	∀v.
69	status_of_pseudo_status M code_memory s sigma policy = s' →
70	set_p1_latch (BitVectorTrie Byte 16)
71	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
72	s' v =
73	status_of_pseudo_status M code_memory
74	(set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
75	#M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
76	qed.
77
78	lemma set_p3_latch_status_of_pseudo_status:
79	∀M.
80	∀code_memory.
81	∀sigma.
82	∀policy.
83	∀s, s'.
84	∀v.
85	status_of_pseudo_status M code_memory s sigma policy = s' →
86	set_p3_latch (BitVectorTrie Byte 16)
87	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
88	s' v =
89	status_of_pseudo_status M code_memory
90	(set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
91	#M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl //
92	qed.
93
94	definition map_acc_a_using_internal_pseudo_address_map:
95	∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
96	λM, sigma, v.
97	match \snd M with
98	[ None ⇒ v
99	\| Some upper_lower_addr ⇒
100	let 〈upper_lower, addr〉 ≝ upper_lower_addr in
101	if eq_upper_lower upper_lower upper then
102	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
103	high
104	else
105	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
106	low
107	].
108
109	(CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... )
110	definition map_internal_ram_address_using_pseudo_address_map:
111	∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
112	λM: internal_pseudo_address_map.
113	λsigma: Word → Word.
114	λaddress: Byte.
115	λvalue: Byte.
116	match lookup_from_internal_ram … address M with
117	[ None ⇒ value
118	\| Some upper_lower_word ⇒
119	let 〈upper_lower, word〉 ≝ upper_lower_word in
120	if eq_upper_lower upper_lower upper then
121	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
122	high
123	else
124	let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
125	low
126	].
127
128	definition map_address_using_internal_pseudo_address_map:
129	∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
130	λM, sigma, sfr, v.
131	match sfr with
132	[ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
133	\| _ ⇒ v
134	].
135
136	lemma set_index_set_index_overwrite:
137	∀A: Type[0].
138	∀n: nat.
139	∀v: Vector A n.
140	∀index: nat.
141	∀e, e': A.
142	∀proof.
143	∀proof'.
144	set_index A n v index e proof =
145	set_index A n (set_index A n v index e' proof') index e proof.
146	#A #n #v elim v normalize
147	[1:
148	#index #e #e' #absurd cases (lt_to_not_zero … absurd)
149	\|2:
150	#n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
151	normalize //
152	]
153	qed.
154
155	lemma set_index_set_index_commutation:
156	∀A: Type[0].
157	∀n: nat.
158	∀v: Vector A n.
159	∀m, o: nat.
160	∀m_lt_proof: m < n.
161	∀o_lt_proof: o < n.
162	∀e, f: A.
163	m ≠ o →
164	set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
165	set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
166	#A #n #v elim v
167	[1:
168	#m #o #m_lt_proof
169	normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
170	\|2:
171	#n' #hd #tl #inductive_hypothesis
172	#m #o
173	cases m cases o
174	[1:
175	#m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
176	@relevant %
177	\|2,3:
178	#o' normalize //
179	\|4:
180	#m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
181	normalize @eq_f @inductive_hypothesis @nmk #relevant
182	>relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
183	]
184	]
185	qed.
186
187	(* XXX: move elsewhere *)
188	lemma get_index_v_set_index_miss:
189	∀a: Type[0].
190	∀n: nat.
191	∀v: Vector a n.
192	∀i, j: nat.
193	∀e: a.
194	∀i_proof: i < n.
195	∀j_proof: j < n.
196	i ≠ j →
197	get_index_v a n (set_index a n v i e i_proof) j j_proof =
198	get_index_v a n v j j_proof.
199	#a #n #v elim v
200	[1:
201	#i #j #e #i_proof
202	cases (lt_to_not_zero … i_proof)
203	\|2:
204	#n' #hd #tl #inductive_hypothesis #i #j
205	cases i cases j
206	[1:
207	#e #i_proof #j_proof #neq_assm
208	cases (absurd ? (refl … 0) neq_assm)
209	\|2,3:
210	#i' #e #i_proof #j_proof #_ %
211	\|4:
212	#i' #j' #e #i_proof #j_proof #neq_assm
213	@inductive_hypothesis @nmk #eq_assm
214	>eq_assm in neq_assm; #neq_assm
215	cases (absurd ? (refl ??) neq_assm)
216	]
217	]
218	qed.
219
220	lemma get_index_v_set_index_hit:
221	∀A: Type[0].
222	∀n: nat.
223	∀v: Vector A n.
224	∀i: nat.
225	∀e: A.
226	∀i_lt_n_proof: i < n.
227	∀i_lt_n_proof': i < n.
228	get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
229	#A #n #v elim v
230	[1:
231	#i #e #i_lt_n_proof
232	cases (lt_to_not_zero … i_lt_n_proof)
233	\|2:
234	#n' #hd #tl #inductive_hypothesis #i #e
235	cases i
236	[1:
237	#i_lt_n_proof #i_lt_n_proof' %
238	\|2:
239	#i' #i_lt_n_proof' #i_lt_n_proof''
240	whd in ⊢ (??%?); @inductive_hypothesis
241	]
242	]
243	qed.
244
245	lemma set_index_status_of_pseudo_status:
246	∀M, code_memory, sigma, policy, s, sfr, v, v'.
247	map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
248	(set_index Byte 19
249	(special_function_registers_8051 (BitVectorTrie Byte 16)
250	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
251	(status_of_pseudo_status M code_memory s sigma policy))
252	(sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
253	=sfr_8051_of_pseudo_sfr_8051 M
254	(special_function_registers_8051 pseudo_assembly_program code_memory
255	(set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
256	#M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
257	whd in match status_of_pseudo_status; normalize nodelta
258	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
259	inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
260	[1:
261	<sfr_neq_acc_a_assm cases sfr
262	[18:
263	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
264	whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
265	>sndM_refl %
266	]
267	%
268	\|2:
269	inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
270	@pair_elim #high #low #high_low_refl normalize nodelta
271	whd in match set_8051_sfr; normalize nodelta
272	<sfr_neq_acc_a_assm
273	cases sfr in high_low_refl sfr_neq_acc_a_assm;
274	[18,37:
275	@pair_elim #high' #low' #high_low_refl'
276	#high_low_refl
277	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
278	whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
279	>sndM_refl normalize nodelta
280	>eq_upper_lower_refl normalize nodelta
281	[1:
282	#relevant >relevant
283	<set_index_set_index_overwrite in ⊢ (??%?);
284	<set_index_set_index_overwrite in ⊢ (???%);
285	>get_index_v_set_index_hit in high_low_refl';
286	#assm >assm in relevant; normalize nodelta * %
287	\|2:
288	#relevant >relevant
289	<set_index_set_index_overwrite in ⊢ (??%?);
290	<set_index_set_index_overwrite in ⊢ (???%);
291	>get_index_v_set_index_hit in high_low_refl';
292	#assm >assm in relevant; normalize nodelta * %
293	]
294	]
295	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
296	#relevant * >get_index_v_set_index_miss
297	try (% #absurd normalize in absurd; destruct(absurd))
298	>relevant normalize nodelta
299	@set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
300	]
301	qed.
302
303	lemma get_index_v_status_of_pseudo_status:
304	∀M, code_memory, sigma, policy, s, s', sfr.
305	map_address_using_internal_pseudo_address_map M sigma sfr
306	(get_index_v Byte 19
307	(special_function_registers_8051 pseudo_assembly_program code_memory s)
308	(sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
309	get_index_v Byte 19
310	(special_function_registers_8051 (BitVectorTrie Byte 16)
311	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
312	(status_of_pseudo_status M code_memory s sigma policy))
313	(sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
314	#M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
315	whd in match status_of_pseudo_status; normalize nodelta
316	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
317	inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
318	[1:
319	cases sfr
320	[18:
321	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
322	whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
323	>sndM_refl %
324	]
325	%
326	\|2:
327	inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
328	@pair_elim #high #low #high_low_refl normalize nodelta
329	cases sfr
330	[18,37:
331	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
332	whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
333	>sndM_refl normalize nodelta >high_low_refl normalize nodelta
334	>eq_upper_lower_refl normalize nodelta
335	whd in match (set_8051_sfr ?????); //
336	]
337	@get_index_v_set_index_miss whd in ⊢ (?(??%%));
338	@nmk #absurd destruct(absurd)
339	]
340	qed.
341
342	lemma set_8051_sfr_status_of_pseudo_status:
343	∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
344	status_of_pseudo_status M code_memory s sigma policy = s' →
345	map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
346	set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
347	status_of_pseudo_status M code_memory
348	(set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
349	#M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
350	<s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
351	qed.
352
353	(*lemma get_8051_sfr_status_of_pseudo_status:
354	∀M.
355	∀cm, ps, sigma, policy.
356	∀sfr.
357	(sfr = SFR_ACC_A → \snd M = None …) →
358	get_8051_sfr (BitVectorTrie Byte 16)
359	(code_memory_of_pseudo_assembly_program cm sigma policy)
360	(status_of_pseudo_status M cm ps sigma policy) sfr =
361	get_8051_sfr pseudo_assembly_program cm ps sfr.
362	#M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
363	[18: >relevant % ]
364	cases sndM try % * #address
365	whd in match get_8051_sfr;
366	whd in match status_of_pseudo_status; normalize nodelta
367	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
368	cases (eq_upper_lower ??) normalize nodelta
369	@pair_elim #upper #lower #upper_lower_refl
370	@get_index_v_set_index_miss @nmk #relevant
371	normalize in relevant; destruct(relevant)
372	qed.*)
373
374	lemma get_8051_sfr_status_of_pseudo_status:
375	∀M, code_memory, sigma, policy, s, s', s'', sfr.
376	status_of_pseudo_status M code_memory s sigma policy = s' →
377	map_address_using_internal_pseudo_address_map M sigma sfr
378	(get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
379	get_8051_sfr (BitVectorTrie Byte 16)
380	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
381	s' sfr = s''.
382	#M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
383	whd in match get_8051_sfr; normalize nodelta
384	@get_index_v_status_of_pseudo_status %
385	qed.
386
387	lemma get_8052_sfr_status_of_pseudo_status:
388	∀M, code_memory, sigma, policy, s, s', sfr.
389	status_of_pseudo_status M code_memory s sigma policy = s' →
390	(get_8052_sfr (BitVectorTrie Byte 16)
391	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
392	s' sfr =
393	(get_8052_sfr pseudo_assembly_program code_memory s sfr)).
394	#M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
395	qed.
396
397	lemma set_8052_sfr_status_of_pseudo_status:
398	∀M, code_memory, sigma, policy, s, s', sfr, v.
399	status_of_pseudo_status M code_memory s sigma policy = s' →
400	(set_8052_sfr (BitVectorTrie Byte 16)
401	(code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
402	status_of_pseudo_status M code_memory
403	(set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
404	#M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
405	qed.
406
407	definition map_address_Byte_using_internal_pseudo_address_map ≝
408	λM,sigma,d,v.
409	match sfr_of_Byte d with
410	[ None ⇒ v
411	\| Some sfr8051_8052 ⇒
412	match sfr8051_8052 with
413	[ inl sfr ⇒
414	map_address_using_internal_pseudo_address_map M sigma sfr v
415	\| inr _ ⇒ v
416	]
417	].
418
419	lemma set_bit_addressable_sfr_status_of_pseudo_status':
420	let M ≝ pseudo_assembly_program in
421	∀code_memory: M.
422	∀s: PreStatus M code_memory.
423	∀d: Byte.
424	∀v: Byte.
425	Σp: PreStatus M code_memory.
426	∀M.
427	∀sigma.
428	∀policy.
429	∀s'.
430	∀v'.
431	status_of_pseudo_status M code_memory s sigma policy = s' →
432	map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
433	(set_bit_addressable_sfr (BitVectorTrie Byte 16)
434	(code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
435	status_of_pseudo_status M code_memory
436	(set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
437	whd in match map_address_Byte_using_internal_pseudo_address_map;
438	whd in match set_bit_addressable_sfr;
439	normalize nodelta
440	@(let M ≝ pseudo_assembly_program in
441	λcode_memory:M.
442	λs: PreStatus M code_memory.
443	λb: Byte.
444	λv: Byte.
445	match sfr_of_Byte b with
446	[ None ⇒ match not_implemented in False with [ ]
447	\| Some sfr8051_8052 ⇒
448	match sfr8051_8052 with
449	[ inl sfr ⇒
450	match sfr with
451	[ SFR_P1 ⇒
452	let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
453	set_p1_latch ?? s v
454	\| SFR_P3 ⇒
455	let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
456	set_p3_latch ?? s v
457	\| _ ⇒ set_8051_sfr ?? s sfr v ]
458	\| inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
459	normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
460	/2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
461	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
462	#v_refl >v_refl //
463	qed.
464
465	lemma set_bit_addressable_sfr_status_of_pseudo_status:
466	∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
467	∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
468	status_of_pseudo_status M code_memory s sigma policy = s' →
469	map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
470	(set_bit_addressable_sfr (BitVectorTrie Byte 16)
471	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
472	s' d v'
473	=status_of_pseudo_status M code_memory
474	(set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
475	#code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
476	#H @H
477	qed.
478
479	lemma set_low_internal_ram_status_of_pseudo_status:
480	∀cm,sigma,policy,M,s,s',ram.
481	status_of_pseudo_status M cm s sigma policy = s' →
482	set_low_internal_ram (BitVectorTrie Byte 16)
483	(code_memory_of_pseudo_assembly_program cm sigma policy)
484	s'
485	(low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
486	= status_of_pseudo_status M cm
487	(set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
488	#cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
489	qed.
490
491	(* Real axiom ATM *)
492	axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
493	∀M,sigma,cm,s,addr,v,v'.
494	map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
495	insert Byte 7 addr v'
496	(low_internal_ram_of_pseudo_low_internal_ram M sigma
497	(low_internal_ram pseudo_assembly_program cm s))
498	=low_internal_ram_of_pseudo_low_internal_ram M sigma
499	(insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
500
501	lemma insert_low_internal_ram_status_of_pseudo_status:
502	∀M,cm,sigma,policy,s,addr,v,v'.
503	map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
504	insert Byte 7 addr v'
505	(low_internal_ram (BitVectorTrie Byte 16)
506	(code_memory_of_pseudo_assembly_program cm sigma policy)
507	(status_of_pseudo_status M cm s sigma policy))
508	= low_internal_ram_of_pseudo_low_internal_ram M sigma
509	(insert Byte 7 addr v
510	(low_internal_ram pseudo_assembly_program cm s)).
511	/2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
512	qed.
513
514	(* Real axiom ATM *)
515	axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
516	∀M,sigma,cm,s,addr,v,v'.
517	map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
518	insert Byte 7 addr v'
519	(high_internal_ram_of_pseudo_high_internal_ram M sigma
520	(high_internal_ram pseudo_assembly_program cm s))
521	=high_internal_ram_of_pseudo_high_internal_ram M sigma
522	(insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
523
524	lemma insert_high_internal_ram_status_of_pseudo_status:
525	∀M,cm,sigma,policy,s,addr,v,v'.
526	map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
527	insert Byte 7 addr v'
528	(high_internal_ram (BitVectorTrie Byte 16)
529	(code_memory_of_pseudo_assembly_program cm sigma policy)
530	(status_of_pseudo_status M cm s sigma policy))
531	= high_internal_ram_of_pseudo_high_internal_ram M sigma
532	(insert Byte 7 addr v
533	(high_internal_ram pseudo_assembly_program cm s)).
534	/2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
535	qed.
536
537	lemma bit_address_of_register_status_of_pseudo_status:
538	∀M,cm,s,sigma,policy,r.
539	bit_address_of_register …
540	(code_memory_of_pseudo_assembly_program cm sigma policy)
541	(status_of_pseudo_status M cm s sigma policy) r =
542	bit_address_of_register … cm s r.
543	#M #cm #s #sigma #policy #r whd in ⊢ (??%%);
544	>(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
545	@pair_elim #un #ln #_
546	@pair_elim #r1 #r0 #_ %
547	qed.
548
549	(*CSC: provable using the axiom in AssemblyProof, but this one seems more
550	primitive *)
551	axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
552	∀M,sigma,cm,s,s',addr.
553	map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
554	(lookup Byte 7 addr
555	(low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
556	lookup Byte 7 addr
557	(low_internal_ram_of_pseudo_low_internal_ram M sigma
558	(low_internal_ram pseudo_assembly_program cm s)) (zero 8)
559	= s'.
560
561	(*CSC: provable using the axiom in AssemblyProof, but this one seems more
562	primitive *)
563	axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
564	∀M,sigma,cm,s,s',addr.
565	map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
566	(lookup Byte 7 addr
567	(high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
568	lookup Byte 7 addr
569	(high_internal_ram_of_pseudo_high_internal_ram M sigma
570	(high_internal_ram pseudo_assembly_program cm s)) (zero 8)
571	= s'.
572
573	lemma get_register_status_of_pseudo_status:
574	∀M,cm,sigma,policy,s,s',s'',r.
575	status_of_pseudo_status M cm s sigma policy = s' →
576	map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
577	(get_register … cm s r) = s'' →
578	get_register …
579	(code_memory_of_pseudo_assembly_program cm sigma policy)
580	s' r = s''.
581	#M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
582	whd in match get_register; normalize nodelta
583	whd in match status_of_pseudo_status; normalize nodelta
584	>bit_address_of_register_status_of_pseudo_status
585	@(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
586	qed.
587
588	lemma external_ram_status_of_pseudo_status:
589	∀M,cm,s,sigma,policy.
590	external_ram …
591	(code_memory_of_pseudo_assembly_program cm sigma policy)
592	(status_of_pseudo_status M cm s sigma policy) =
593	external_ram … cm s.
594	//
595	qed.
596
597	lemma set_external_ram_status_of_pseudo_status:
598	∀M,cm,ps,sigma,policy,ram.
599	set_external_ram …
600	(code_memory_of_pseudo_assembly_program cm sigma policy)
601	(status_of_pseudo_status M cm ps sigma policy)
602	ram =
603	status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
604	//
605	qed.
606
607	lemma set_register_status_of_pseudo_status:
608	∀M,sigma,policy,cm,s,s',r,v,v'.
609	status_of_pseudo_status M cm s sigma policy = s' →
610	map_internal_ram_address_using_pseudo_address_map M sigma
611	(false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
612	set_register (BitVectorTrie Byte 16)
613	(code_memory_of_pseudo_assembly_program cm sigma policy)
614	s' r v'
615	= status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
616	sigma policy.
617	#M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
618	whd in match set_register; normalize nodelta
619	>bit_address_of_register_status_of_pseudo_status
620	>(insert_low_internal_ram_status_of_pseudo_status … v_ok)
621	@set_low_internal_ram_status_of_pseudo_status %
622	qed.
623
624	definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
625	λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
626	let 〈low,high,accA〉 ≝ M in
627	match addr with
628	[ INDIRECT i ⇒
629	lookup_opt …
630	(bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None …
631	\| EXT_INDIRECT e ⇒
632	lookup_opt …
633	(bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None …
634	\| ACC_DPTR ⇒
635	(* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
636	in the ACC_A *)
637	map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
638	get_8051_sfr … cm s SFR_ACC_A
639	\| ACC_PC ⇒
640	(* XXX: as above *)
641	map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
642	get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
643	\| _ ⇒ True ].
644
645	definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
646	λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
647	match addr with
648	[ DIRECT d ⇒
649	let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
650	match head' … bit_one with
651	[ true ⇒
652	map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
653	\| false ⇒
654	map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
655	\| INDIRECT i ⇒
656	let register ≝ get_register ?? s [[ false; false; i ]] in
657	map_internal_ram_address_using_pseudo_address_map M sigma register v
658	\| REGISTER r ⇒
659	map_internal_ram_address_using_pseudo_address_map M sigma
660	(false:::bit_address_of_register … s r) v
661	\| ACC_A ⇒
662	map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
663	\| _ ⇒ v ].
664
665	(CSC: move elsewhere)
666	lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
667	#A #n #v inversion v in ⊢ ?;
668	[ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
669	\| #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
670	qed.
671
672	(CSC: move elsewhere)
673	lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
674	#A #v inversion v in ⊢ ?;
675	[ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
676	\| #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
677	/2 by jmeq_to_eq/
678	]
679	qed.
680
681	(CSC: move elsewhere)
682	lemma eq_cons_head_append:
683	∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
684	head' A 0 hd:::tl = hd@@tl.
685	#A #n #hd #tl >(eq_head' … hd) >tail_singleton %
686	qed.
687
688	lemma set_arg_8_status_of_pseudo_status':
689	∀cm.
690	∀ps.
691	∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
692	∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
693	status_of_pseudo_status M cm ps sigma policy = s' →
694	map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
695	map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
696	set_arg_8 (BitVectorTrie Byte 16)
697	(code_memory_of_pseudo_assembly_program cm sigma policy)
698	s' addr value' =
699	status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
700	whd in match set_arg_8; normalize nodelta
701	@(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
702	acc_a ; acc_b ; ext_indirect ;
703	ext_indirect_dptr ]]. λv.
704	match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
705	acc_a ; acc_b ; ext_indirect ;
706	ext_indirect_dptr ]] addr) →
707	Σp.?
708	with
709	[ DIRECT d ⇒
710	λdirect: True.
711	deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
712	match head' … bit_one with
713	[ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
714	\| false ⇒
715	let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
716	set_low_internal_ram ?? s memory
717	]
718
719	\| INDIRECT i ⇒
720	λindirect: True.
721	let register ≝ get_register ?? s [[ false; false; i ]] in
722	let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
723	match head' … bit_one with
724	[ false ⇒
725	let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
726	set_low_internal_ram ?? s memory
727	\| true ⇒
728	let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
729	set_high_internal_ram ?? s memory
730	]
731	\| REGISTER r ⇒ λregister: True. set_register ?? s r v
732	\| ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
733	\| ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
734	\| EXT_INDIRECT e ⇒
735	λext_indirect: True.
736	let address ≝ get_register ?? s [[ false; false; e ]] in
737	let padded_address ≝ pad 8 8 address in
738	let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
739	set_external_ram ?? s memory
740	\| EXT_INDIRECT_DPTR ⇒
741	λext_indirect_dptr: True.
742	let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
743	let memory ≝ insert ? 16 address v (external_ram ?? s) in
744	set_external_ram ?? s memory
745	\| _ ⇒
746	λother: False.
747	match other in False with [ ]
748	] (subaddressing_modein … a)) normalize nodelta
749	#M #sigma #policy #s' #v' #s_refl <s_refl
750	whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
751	whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
752	[1,2:
753	<vsplit_refl normalize nodelta >p normalize nodelta
754	[ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
755	\| #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
756	\|3,4: cases M * -M #low #high #accA normalize nodelta
757	#EQ1 #EQ2 change with (get_register ????) in match register in p;
758	>(get_register_status_of_pseudo_status … (refl …) (refl …))
759	whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
760	whd in match (lookup_from_internal_ram ??);
761	>EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
762	[ >(insert_high_internal_ram_status_of_pseudo_status … v)
763	\| >(insert_low_internal_ram_status_of_pseudo_status … v) ]
764	// <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
765	\|5: cases M * -M #low #high #accA normalize nodelta
766	#EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
767	whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
768	whd in match lookup_from_internal_ram; normalize nodelta
769	>EQ1 normalize nodelta
770	>external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
771	\|6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
772	\|7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
773	\|8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
774	\|9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
775	>(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
776	>external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
777	qed.
778
779	lemma set_arg_8_status_of_pseudo_status:
780	∀cm.
781	∀ps.
782	∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
783	∀value.
784	∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
785	addr = addr' →
786	status_of_pseudo_status M cm ps sigma policy = s' →
787	map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
788	map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
789	set_arg_8 (BitVectorTrie Byte 16)
790	(code_memory_of_pseudo_assembly_program cm sigma policy)
791	s' addr value' =
792	status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
793	#cm #ps #addr #addr' #value
794	cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
795	#M #sigma #policy #s' #value' #addr_refl <addr_refl
796	@relevant
797	qed.
798
799	lemma p1_latch_status_of_pseudo_status:
800	∀M.
801	∀sigma.
802	∀policy.
803	∀code_memory: pseudo_assembly_program.
804	∀s: PreStatus … code_memory.
805	∀s'.
806	(status_of_pseudo_status M code_memory s sigma policy) = s' →
807	(p1_latch (BitVectorTrie Byte 16)
808	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
809	s' =
810	(p1_latch pseudo_assembly_program code_memory s)).
811	#M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
812	qed.
813
814	lemma p3_latch_status_of_pseudo_status:
815	∀M.
816	∀sigma.
817	∀policy.
818	∀code_memory: pseudo_assembly_program.
819	∀s: PreStatus … code_memory.
820	∀s'.
821	(status_of_pseudo_status M code_memory s sigma policy) = s' →
822	(p3_latch (BitVectorTrie Byte 16)
823	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
824	(status_of_pseudo_status M code_memory s sigma policy) =
825	(p3_latch pseudo_assembly_program code_memory s)).
826	#M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
827	qed.
828
829	lemma get_bit_addressable_sfr_status_of_pseudo_status':
830	let M ≝ pseudo_assembly_program in
831	∀code_memory: M.
832	∀s: PreStatus M code_memory.
833	∀d: Byte.
834	∀l: bool.
835	Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
836	status_of_pseudo_status M code_memory s sigma policy = s' →
837	(get_bit_addressable_sfr (BitVectorTrie Byte 16)
838	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
839	s' d l =
840	map_address_Byte_using_internal_pseudo_address_map M sigma
841	d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
842	whd in match get_bit_addressable_sfr;
843	whd in match map_address_Byte_using_internal_pseudo_address_map;
844	normalize nodelta
845	@(let M ≝ pseudo_assembly_program in
846	λcode_memory:M.
847	λs: PreStatus M code_memory.
848	λb: Byte.
849	λl: bool.
850	match sfr_of_Byte b with
851	[ None ⇒ match not_implemented in False with [ ]
852	\| Some sfr8051_8052 ⇒
853	match sfr8051_8052 with
854	[ inl sfr ⇒
855	match sfr with
856	[ SFR_P1 ⇒
857	if l then
858	p1_latch … s
859	else
860	get_8051_sfr … s SFR_P1
861	\| SFR_P3 ⇒
862	if l then
863	p3_latch … s
864	else
865	get_8051_sfr … s SFR_P3
866	\| _ ⇒ get_8051_sfr … s sfr
867	]
868	\| inr sfr ⇒ get_8052_sfr M code_memory s sfr
869	]
870	])
871	#M #sigma #policy #s' #s_refl <s_refl normalize nodelta
872	/2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
873	qed.
874
875	lemma get_bit_addressable_sfr_status_of_pseudo_status:
876	let M ≝ pseudo_assembly_program in
877	∀code_memory: M.
878	∀s: PreStatus M code_memory.
879	∀d: Byte.
880	∀l: bool.
881	∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
882	map_address_Byte_using_internal_pseudo_address_map M sigma
883	d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
884	(status_of_pseudo_status M code_memory s sigma policy) = s' →
885	(get_bit_addressable_sfr (BitVectorTrie Byte 16)
886	(code_memory_of_pseudo_assembly_program code_memory sigma policy)
887	s' d l) = s''.
888	#code #s #d #v
889	cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
890	#M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
891	qed.
892
893	lemma program_counter_status_of_pseudo_status:
894	∀M. ∀sigma: Word → Word. ∀policy.
895	∀code_memory: pseudo_assembly_program.
896	∀s: PreStatus ? code_memory.
897	∀s'.
898	∀s''.
899	sigma (program_counter … s) = s'' →
900	(status_of_pseudo_status M code_memory s sigma policy) = s' →
901	program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
902	s' = s''.
903	#M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
904	qed.
905
906	lemma get_cy_flag_status_of_pseudo_status:
907	∀M, cm, sigma, policy, s, s'.
908	(status_of_pseudo_status M cm s sigma policy) = s' →
909	(get_cy_flag (BitVectorTrie Byte 16)
910	(code_memory_of_pseudo_assembly_program cm sigma policy)
911	s' =
912	get_cy_flag pseudo_assembly_program cm s).
913	#M #cm #sigma #policy #s #s' #s_refl <s_refl
914	whd in match get_cy_flag; normalize nodelta
915	>(get_index_v_status_of_pseudo_status … (refl …)) %
916	qed.
917
918	lemma get_arg_8_status_of_pseudo_status':
919	∀cm.
920	∀ps.
921	∀l.
922	∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
923	Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
924	(status_of_pseudo_status M cm ps sigma policy) = s' →
925	map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
926	get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
927	s' l addr =
928	map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
929	whd in match get_arg_8; normalize nodelta
930	@(let m ≝ pseudo_assembly_program in
931	λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]].
932	match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with
933	[ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
934	\| ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
935	\| DATA d ⇒ λdata: True. d
936	\| REGISTER r ⇒ λregister: True. get_register ?? s r
937	\| EXT_INDIRECT_DPTR ⇒
938	λext_indirect_dptr: True.
939	let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
940	lookup ? 16 address (external_ram ?? s) (zero 8)
941	\| EXT_INDIRECT e ⇒
942	λext_indirect: True.
943	let address ≝ get_register ?? s [[ false; false; e ]] in
944	let padded_address ≝ pad 8 8 address in
945	lookup ? 16 padded_address (external_ram ?? s) (zero 8)
946	\| ACC_DPTR ⇒
947	λacc_dptr: True.
948	let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
949	let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
950	let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
951	lookup ? 16 address (external_ram ?? s) (zero 8)
952	\| ACC_PC ⇒
953	λacc_pc: True.
954	let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
955	let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
956	lookup ? 16 address (external_ram ?? s) (zero 8)
957	\| DIRECT d ⇒
958	λdirect: True.
959	let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
960	match head' … hd with
961	[ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
962	\| false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
963	]
964	\| INDIRECT i ⇒
965	λindirect: True.
966	let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
967	match head' … hd with
968	[ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
969	\| false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
970	]
971	\| _ ⇒ λother: False.
972	match other in False with [ ]
973	] (subaddressing_modein … a)) normalize nodelta
974	#M #sigma #policy #s' #s_refl <s_refl
975	whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
976	whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
977	[1:
978	#_ >p normalize nodelta >p1 normalize nodelta
979	@(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
980	\|2:
981	#_>p normalize nodelta >p1 normalize nodelta
982	@(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
983	\|3,4: cases M -M * #low #high #accA
984	#assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
985	whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
986	whd in match lookup_from_internal_ram; normalize nodelta
987	>assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
988	[1:
989	@(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma)
990	\|2:
991	@(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma)
992	]
993	@eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
994	\|5: cases M -M * #low #high #accA
995	#assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
996	whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
997	whd in match lookup_from_internal_ram; normalize nodelta
998	>assoc_list_assm normalize nodelta %
999	\|6,7,8,9:
1000	#_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
1001	\|10: cases M -M * #low #high #accA
1002	#acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1003	>(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1004	>(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1005	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1006	>acc_a_assm >p normalize nodelta //
1007	\|11: cases M -M * #low #high #accA
1008	* #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1009	>(program_counter_status_of_pseudo_status … (refl …) (refl …))
1010	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1011	>sigma_assm >map_acc_a_assm >p normalize nodelta //
1012	\|12:
1013	#_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1014	>(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1015	>external_ram_status_of_pseudo_status //
1016	]
1017	qed.
1018
1019	lemma get_arg_8_status_of_pseudo_status:
1020	∀cm.
1021	∀ps.
1022	∀l.
1023	∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
1024	∀M. ∀sigma. ∀policy. ∀s', s''.
1025	(status_of_pseudo_status M cm ps sigma policy) = s' →
1026	map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
1027	map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
1028	get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1029	s' l addr = s''.
1030	#cm #ps #l #addr
1031	cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
1032	#M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
1033	@relevant assumption
1034	qed.
1035
1036	lemma get_arg_16_status_of_pseudo_status:
1037	∀cm.
1038	∀ps.
1039	∀addr: [[data16]].
1040	∀M. ∀sigma. ∀policy. ∀s'.
1041	status_of_pseudo_status M cm ps sigma policy = s' →
1042	get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1043	s' addr =
1044	(get_arg_16 … cm ps addr).
1045	#cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
1046	qed.
1047
1048	lemma set_arg_16_status_of_pseudo_status:
1049	∀cm.
1050	∀ps.
1051	∀addr,addr': [[dptr]].
1052	∀v,v': Word.
1053	∀M. ∀sigma. ∀policy. ∀s'.
1054	status_of_pseudo_status M cm ps sigma policy = s' →
1055	v=v' → addr=addr' →
1056	set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1057	s' v' addr' =
1058	status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
1059	#cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
1060	<addr_refl #v_refl <v_refl
1061	@(subaddressing_mode_elim … addr)
1062	whd in match set_arg_16; normalize nodelta
1063	whd in match set_arg_16'; normalize nodelta
1064	@(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
1065	@set_8051_sfr_status_of_pseudo_status try % @sym_eq
1066	@set_8051_sfr_status_of_pseudo_status %
1067	qed.
1068
1069	definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
1070	λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
1071	match addr with
1072	[ BIT_ADDR b ⇒
1073	let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1074	match head' … bit_1 with
1075	[ true ⇒
1076	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1077	let trans ≝ true:::four_bits @@ [[false; false; false]] in
1078	map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1079	\| false ⇒
1080	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1081	let address' ≝ [[true; false; false]]@@four_bits in
1082	let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1083	map_internal_ram_address_using_pseudo_address_map M sigma
1084	(false:::address') t = t
1085	]
1086	\| N_BIT_ADDR b ⇒
1087	let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1088	match head' … bit_1 with
1089	[ true ⇒
1090	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1091	let trans ≝ true:::four_bits @@ [[false; false; false]] in
1092	map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1093	\| false ⇒
1094	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1095	let address' ≝ [[true; false; false]]@@four_bits in
1096	let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1097	map_internal_ram_address_using_pseudo_address_map M sigma
1098	(false:::address') t = t
1099	]
1100	\| _ ⇒ True ].
1101
1102	lemma get_arg_1_status_of_pseudo_status':
1103	∀cm.
1104	∀ps.
1105	∀addr: [[bit_addr; n_bit_addr; carry]].
1106	∀l.
1107	Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
1108	status_of_pseudo_status M cm ps sigma policy = s' →
1109	map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1110	get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1111	s' addr l =
1112	(get_arg_1 … cm ps addr l).
1113	whd in match get_arg_1; normalize nodelta
1114	@(let m ≝ pseudo_assembly_program in
1115	λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
1116	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1117	n_bit_addr ;
1118	carry ]] x) → Σb: bool. ? with
1119	[ BIT_ADDR b ⇒
1120	λbit_addr: True.
1121	let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1122	match head' … bit_1 with
1123	[ true ⇒
1124	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1125	let trans ≝ true:::four_bits @@ [[false; false; false]] in
1126	let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1127	get_index_v … sfr (nat_of_bitvector … three_bits) ?
1128	\| false ⇒
1129	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1130	let address' ≝ [[true; false; false]]@@four_bits in
1131	let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1132	get_index_v … t (nat_of_bitvector … three_bits) ?
1133	]
1134	\| N_BIT_ADDR n ⇒
1135	λn_bit_addr: True.
1136	let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1137	match head' … bit_1 with
1138	[ true ⇒
1139	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1140	let trans ≝ true:::four_bits @@ [[false; false; false]] in
1141	let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1142	¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
1143	\| false ⇒
1144	let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1145	let address' ≝ [[true; false; false]]@@four_bits in
1146	let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1147	¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
1148	]
1149	\| CARRY ⇒ λcarry: True. get_cy_flag ?? s
1150	\| _ ⇒ λother.
1151	match other in False with [ ]
1152	] (subaddressing_modein … a)) normalize nodelta
1153	[4,5,8,9: //]
1154	#M #sigma #policy #s' #s_refl <s_refl
1155	[1:
1156	#_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
1157	\|2,4:
1158	whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2
1159	normalize nodelta
1160	>(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
1161	>map_address_assm %
1162	\|3,5:
1163	whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1164	whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta
1165	>(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1166	#map_address_assm >map_address_assm %
1167	]
1168	qed.
1169
1170	lemma get_arg_1_status_of_pseudo_status:
1171	∀cm.
1172	∀ps.
1173	∀addr, addr': [[bit_addr; n_bit_addr; carry]].
1174	∀l.
1175	∀M. ∀sigma. ∀policy. ∀s'.
1176	addr = addr' →
1177	status_of_pseudo_status M cm ps sigma policy = s' →
1178	map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1179	get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1180	s' addr l =
1181	(get_arg_1 … cm ps addr' l).
1182	#cm #ps #addr #addr' #l
1183	cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
1184	#M #sigma #policy #s' #addr_refl <addr_refl
1185	@assm
1186	qed.
1187
1188	(*CSC: daemon
1189	definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
1190	λM: internal_pseudo_address_map.
1191	λcm: pseudo_assembly_program.
1192	λs: PreStatus ? cm.
1193	λsigma: Word → Word.
1194	λaddr: [[bit_addr; carry]].
1195	λv: Bit.
1196	match addr with
1197	[ BIT_ADDR b ⇒
1198	let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1199	match head' … bit_1 with
1200	[ true ⇒
1201	let address ≝ nat_of_bitvector … seven_bits in
1202	let d ≝ address ÷ 8 in
1203	let m ≝ address mod 8 in
1204	let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1205	let sfr ≝ get_bit_addressable_sfr … s t true in
1206	map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
1207	\| false ⇒
1208	let address ≝ nat_of_bitvector … seven_bits in
1209	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1210	let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1211	map_internal_ram_address_using_pseudo_address_map M sigma
1212	(false:::address') t = t
1213	]
1214	\| CARRY ⇒ True
1215	\| _ ⇒ True
1216	].
1217
1218	definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
1219	λM: internal_pseudo_address_map.
1220	λcm: pseudo_assembly_program.
1221	λs: PreStatus ? cm.
1222	λsigma: Word → Word.
1223	λaddr: [[bit_addr; carry]].
1224	λv: Bit.
1225	match addr with
1226	[ BIT_ADDR b ⇒
1227	let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1228	match head' … bit_1 with
1229	[ true ⇒
1230	let address ≝ nat_of_bitvector … seven_bits in
1231	let d ≝ address ÷ 8 in
1232	let m ≝ address mod 8 in
1233	let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1234	let sfr ≝ get_bit_addressable_sfr … s t true in
1235	let new_sfr ≝ set_index … sfr m v ? in
1236	map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
1237	\| false ⇒
1238	let address ≝ nat_of_bitvector … seven_bits in
1239	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1240	let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1241	let n_bit ≝ set_index … t (modulus address 8) v ? in
1242	let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1243	map_internal_ram_address_using_pseudo_address_map M sigma
1244	(false:::address') n_bit = n_bit
1245	]
1246	\| CARRY ⇒ True
1247	\| _ ⇒ True
1248	].
1249	@modulus_less_than
1250	qed.
1251
1252	lemma set_arg_1_status_of_pseudo_status':
1253	∀cm: pseudo_assembly_program.
1254	∀ps: PreStatus pseudo_assembly_program cm.
1255	∀addr: [[bit_addr; carry]].
1256	∀b: Bit.
1257	Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1258	b = b' →
1259	status_of_pseudo_status M cm ps sigma policy = s' →
1260	map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1261	map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1262	set_arg_1 (BitVectorTrie Byte 16)
1263	(code_memory_of_pseudo_assembly_program cm sigma policy)
1264	s' addr b =
1265	status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1266	whd in match set_arg_1; normalize nodelta
1267	whd in ⊢ (? → ? → ? → ? → ??(λx.? → ? → ? → ? → ? → ? → ? → %?????? → %?????? → ?));
1268	normalize nodelta
1269	@(let m ≝ pseudo_assembly_program in
1270	λcm.
1271	λs: PreStatus m cm.
1272	λa: [[bit_addr; carry]].
1273	λv: Bit.
1274	match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
1275	[ BIT_ADDR b ⇒ λbit_addr: True.
1276	let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1277	match head' … bit_1 with
1278	[ true ⇒
1279	let address ≝ nat_of_bitvector … seven_bits in
1280	let d ≝ address ÷ 8 in
1281	let m ≝ address mod 8 in
1282	let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1283	let sfr ≝ get_bit_addressable_sfr … s t true in
1284	let new_sfr ≝ set_index … sfr m v ? in
1285	set_bit_addressable_sfr … s new_sfr t
1286	\| false ⇒
1287	let address ≝ nat_of_bitvector … seven_bits in
1288	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1289	let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1290	let n_bit ≝ set_index … t (modulus address 8) v ? in
1291	let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1292	set_low_internal_ram … s memory
1293	]
1294	\| CARRY ⇒
1295	λcarry: True.
1296	let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1297	let new_psw ≝ v:::seven_bits in
1298	set_8051_sfr ?? s SFR_PSW new_psw
1299	\| _ ⇒
1300	λother: False.
1301	match other in False with
1302	[ ]
1303	] (subaddressing_modein … a)) normalize nodelta
1304	try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
1305	[1:
1306	#_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1307	whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1308	>p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
1309	\|2,3:
1310	>p normalize nodelta >p1 normalize nodelta
1311	#map_bit_address_assm_1 #map_bit_address_assm_2
1312	[1:
1313	>(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
1314	>map_bit_address_assm_1
1315	>(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
1316	\|2:
1317	whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
1318	>(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1319	>map_bit_address_assm_1
1320	>(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
1321	>set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
1322	]
1323	]
1324	qed.
1325
1326	lemma set_arg_1_status_of_pseudo_status:
1327	∀cm: pseudo_assembly_program.
1328	∀ps: PreStatus pseudo_assembly_program cm.
1329	∀addr: [[bit_addr; carry]].
1330	∀b: Bit.
1331	∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1332	b = b' →
1333	status_of_pseudo_status M cm ps sigma policy = s' →
1334	map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1335	map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1336	set_arg_1 (BitVectorTrie Byte 16)
1337	(code_memory_of_pseudo_assembly_program cm sigma policy)
1338	s' addr b =
1339	status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1340	#cm #ps #addr #b
1341	cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
1342	@relevant
1343	qed.*)
1344
1345	lemma clock_status_of_pseudo_status:
1346	∀M,cm,sigma,policy,s,s'.
1347	(status_of_pseudo_status M cm s sigma policy) = s' →
1348	clock …
1349	(code_memory_of_pseudo_assembly_program cm sigma policy)
1350	s'
1351	= clock … cm s.
1352	#M #cm #sigma #policy #s #s' #s_refl <s_refl //
1353	qed.
1354
1355	lemma set_clock_status_of_pseudo_status:
1356	∀M,cm,sigma,policy,s,s',v,v'.
1357	status_of_pseudo_status M cm s sigma policy = s' →
1358	v = v' →
1359	set_clock …
1360	(code_memory_of_pseudo_assembly_program cm sigma policy)
1361	s' v
1362	= status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
1363	#M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
1364	qed.
1365
1366	(*CSC: daemon
1367	lemma set_flags_status_of_pseudo_status:
1368	∀M.
1369	∀sigma.
1370	∀policy.
1371	∀code_memory: pseudo_assembly_program.
1372	∀s: PreStatus ? code_memory.
1373	∀s'.
1374	∀b, b': Bit.
1375	∀opt, opt': option Bit.
1376	∀c, c': Bit.
1377	b = b' →
1378	opt = opt' →
1379	c = c' →
1380	status_of_pseudo_status M code_memory s sigma policy = s' →
1381	set_flags … s' b opt c =
1382	status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
1383	#M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
1384	#b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
1385	whd in match status_of_pseudo_status; normalize nodelta
1386	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1387	cases (\snd M)
1388	[1:
1389	normalize nodelta %
1390	\|2: ** #address normalize nodelta
1391	@(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1392	whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
1393	@split_eq_status try % whd in match (sfr_8051_index ?);
1394	cases daemon
1395	]
1396	qed.*)
1397
1398	lemma get_ac_flag_status_of_pseudo_status:
1399	∀M: internal_pseudo_address_map.
1400	∀sigma: Word → Word.
1401	∀policy: Word → bool.
1402	∀code_memory: pseudo_assembly_program.
1403	∀s: PreStatus ? code_memory.
1404	∀s'.
1405	status_of_pseudo_status M code_memory s sigma policy = s' →
1406	get_ac_flag ?? s' = get_ac_flag ? code_memory s.
1407	#M #sigma #policy #code_memory #s #s' #s_refl <s_refl
1408	whd in match get_ac_flag; normalize nodelta
1409	whd in match status_of_pseudo_status; normalize nodelta
1410	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1411	cases (\snd M) try % normalize nodelta ** normalize nodelta
1412	#address
1413	@(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1414	whd in match sfr_8051_index; normalize nodelta
1415	>get_index_v_set_index_miss [2,4: /2/] %
1416	qed.
1417
1418	lemma get_ov_flag_status_of_pseudo_status:
1419	∀M: internal_pseudo_address_map.
1420	∀sigma: Word → Word.
1421	∀policy: Word → bool.
1422	∀code_memory: pseudo_assembly_program.
1423	∀s: PreStatus ? code_memory.
1424	∀s'.
1425	status_of_pseudo_status M code_memory s sigma policy = s' →
1426	get_ov_flag ?? s' = get_ov_flag ? code_memory s.
1427	#M #sigma #policy #code_memory #s #s' #s_refl <s_refl
1428	whd in match get_ov_flag; normalize nodelta
1429	whd in match status_of_pseudo_status; normalize nodelta
1430	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1431	cases (\snd M) try %
1432	** normalize nodelta #address
1433	@(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1434	whd in match sfr_8051_index; normalize nodelta
1435	>get_index_v_set_index_miss [2,4: /2/] %
1436	qed.
1437
1438	(*CSC: useless?
1439	lemma get_arg_8_pseudo_addressing_mode_ok:
1440	∀M: internal_pseudo_address_map.
1441	∀cm: pseudo_assembly_program.
1442	∀ps: PreStatus pseudo_assembly_program cm.
1443	∀sigma: Word → Word.
1444	∀policy: Word → bool.
1445	∀addr1: [[registr; direct]].
1446	assert_data pseudo_assembly_program M cm ps addr1 = true →
1447	get_arg_8 (BitVectorTrie Byte 16)
1448	(code_memory_of_pseudo_assembly_program cm sigma policy)
1449	(status_of_pseudo_status M cm ps sigma policy) true addr1 =
1450	get_arg_8 pseudo_assembly_program cm ps true addr1.
1451	[2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1452	#M #cm #ps #sigma #policy #addr1
1453	@(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
1454	[1:
1455	whd in ⊢ (??%? → ??%?);
1456	whd in match bit_address_of_register; normalize nodelta
1457	@pair_elim #un #ln #un_ln_refl
1458	lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
1459	@(pair_replace ?????????? un_ln_refl)
1460	[1:
1461	whd in match get_8051_sfr; normalize nodelta
1462	whd in match sfr_8051_index; normalize nodelta
1463	@eq_f <get_index_v_special_function_registers_8051_not_acc_a
1464	try % #absurd destruct(absurd)
1465	\|2:
1466	#assembly_mode_ok_refl
1467	>low_internal_ram_of_pseudo_internal_ram_miss
1468	[1:
1469	%
1470	\|2:
1471	cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
1472	[1:
1473	#absurd destruct(absurd)
1474	\|2:
1475	* normalize nodelta
1476	[1:
1477	\|2:
1478	#_ #absurd destruct(absurd)
1479	]
1480	#absurd try % @sym_eq assumption
1481	]
1482	]
1483	\|2:
1484	#addressing_mode_ok_refl whd in ⊢ (??%?);
1485	@pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX cases daemon (*
1486	@pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
1487	inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
1488	[1:
1489	whd in ⊢ (??%%); normalize nodelta
1490	cases (eqb ??) normalize nodelta [1: % ]
1491	cases (eqb ??) normalize nodelta [1: % ]
1492	cases (eqb ??) normalize nodelta [1: % ]
1493	cases (eqb ??) normalize nodelta [1: % ]
1494	cases (eqb ??) normalize nodelta [1:
1495	@get_8051_sfr_status_of_pseudo_status
1496	#absurd destruct(absurd)
1497	]
1498	cases (eqb ??) normalize nodelta [1:
1499	@get_8051_sfr_status_of_pseudo_status
1500	#absurd destruct(absurd)
1501	]
1502	cases (eqb ??) normalize nodelta [1:
1503	@get_8051_sfr_status_of_pseudo_status
1504	#absurd destruct(absurd)
1505	]
1506	cases (eqb ??) normalize nodelta [1:
1507	@get_8051_sfr_status_of_pseudo_status
1508	#absurd destruct(absurd)
1509	]
1510	cases (eqb ??) normalize nodelta [1:
1511	@get_8051_sfr_status_of_pseudo_status
1512	#absurd destruct(absurd)
1513	]
1514	cases (eqb ??) normalize nodelta [1: % ]
1515	cases (eqb ??) normalize nodelta [1: % ]
1516	cases (eqb ??) normalize nodelta [1: % ]
1517	cases (eqb ??) normalize nodelta [1: % ]
1518	cases (eqb ??) normalize nodelta [1: % ]
1519	cases (eqb ??) normalize nodelta [1:
1520	@get_8051_sfr_status_of_pseudo_status
1521	#absurd destruct(absurd)
1522	]
1523	cases (eqb ??) normalize nodelta [1:
1524	@get_8051_sfr_status_of_pseudo_status
1525	#absurd destruct(absurd)
1526	]
1527	cases (eqb ??) normalize nodelta [1:
1528	@get_8051_sfr_status_of_pseudo_status
1529	#absurd destruct(absurd)
1530	]
1531	cases (eqb ??) normalize nodelta [1:
1532	@get_8051_sfr_status_of_pseudo_status
1533	#absurd destruct(absurd)
1534	]
1535	cases (eqb ??) normalize nodelta [1:
1536	@get_8051_sfr_status_of_pseudo_status
1537	#absurd destruct(absurd)
1538	]
1539	cases (eqb ??) normalize nodelta [1:
1540	@get_8051_sfr_status_of_pseudo_status
1541	#absurd destruct(absurd)
1542	]
1543	cases (eqb ??) normalize nodelta [1:
1544	@get_8051_sfr_status_of_pseudo_status
1545	#absurd destruct(absurd)
1546	]
1547	cases (eqb ??) normalize nodelta [1:
1548	@get_8051_sfr_status_of_pseudo_status
1549	#absurd destruct(absurd)
1550	]
1551	cases (eqb ??) normalize nodelta [1:
1552	@get_8051_sfr_status_of_pseudo_status
1553	#absurd destruct(absurd)
1554	]
1555	cases (eqb ??) normalize nodelta [1:
1556	@get_8051_sfr_status_of_pseudo_status
1557	#absurd destruct(absurd)
1558	]
1559	inversion (eqb ??) #eqb_refl normalize nodelta [1:
1560	@get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
1561	whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
1562	>bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
1563	#assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
1564	#relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
1565	]
1566	cases (eqb ??) normalize nodelta [1:
1567	@get_8051_sfr_status_of_pseudo_status
1568	#absurd destruct(absurd)
1569	] %
1570	\|2:
1571	lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
1572	whd in match status_of_pseudo_status; normalize nodelta
1573	>low_internal_ram_of_pseudo_internal_ram_miss try %
1574	cut(arg = false:::(three_bits@@nl))
1575	[1:
1576	<get_index_v_refl
1577	cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
1578	[1:
1579	cut(ignore = [[get_index_v bool 4 nu 0 ?]])
1580	[1:
1581	@le_S_S @le_O_n
1582	\|2:
1583	cut(ignore = \fst (vsplit bool 1 3 nu))
1584	[1:
1585	>ignore_three_bits_refl %
1586	\|2:
1587	#ignore_refl >ignore_refl
1588	cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
1589	>nu_refl %
1590	]
1591	\|3:
1592	#ignore_refl >ignore_refl in ignore_three_bits_refl;
1593	#relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
1594	#nu_refl <nu_refl %
1595	]
1596	\|2:
1597	#nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
1598	@sym_eq @vsplit_ok >nu_nl_refl %
1599	]
1600	\|2:
1601	#arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
1602	normalize nodelta
1603	[1:
1604	cases (eq_bv ???) normalize #absurd destruct(absurd)
1605	\|2:
1606	#_ %
1607	]
1608	]
1609	]
1610	]
1611	qed.))
1612
1613	lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
1614	∀M, cm, ps, sigma, x.
1615	∀addr1: [[acc_a]].
1616	assert_data pseudo_assembly_program M cm ps addr1=true →
1617	map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
1618	#M #cm #ps #sigma #x #addr1
1619	@(subaddressing_mode_elim … addr1)
1620	whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//]
1621	* #upper_lower #address normalize nodelta #absurd destruct(absurd)
1622	qed.
1623
1624	lemma addressing_mode_ok_to_snd_M_data:
1625	∀M, cm, ps.
1626	∀addr: [[acc_a]].
1627	assert_data pseudo_assembly_program M cm ps addr = true →
1628	\snd M = None ….
1629	#M #cm #ps #addr
1630	@(subaddressing_mode_elim … addr)
1631	whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta
1632	[ #_ %
1633	\| #addr #abs destruct(abs) ]
1634	qed.
1635
1636	((CSC: move elsewhere*)
1637	lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
1638	∀A, B: Type[0].
1639	∀e: A.
1640	∀the_list: list (A × B).
1641	∀eq_f: A → A → bool.
1642	assoc_list_exists A B e eq_f the_list = true →
1643	∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
1644	#A #B #e #the_list #eq_f elim the_list
1645	[1:
1646	whd in ⊢ (??%? → ?); #absurd destruct(absurd)
1647	\|2:
1648	#hd #tl #inductive_hypothesis
1649	whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
1650	cases (eq_f (\fst hd) e) normalize nodelta
1651	[1:
1652	#_ %{(\snd hd)} %
1653	\|2:
1654	@inductive_hypothesis
1655	]
1656	]
1657	qed.
1658
1659	(CSC: move elsewhere)
1660	lemma assoc_list_exists_false_to_assoc_list_lookup_None:
1661	∀A, B: Type[0].
1662	∀e, e': A.
1663	∀the_list, the_list': list (A × B).
1664	∀eq_f: A → A → bool.
1665	e = e' →
1666	the_list = the_list' →
1667	assoc_list_exists A B e eq_f the_list = false →
1668	assoc_list_lookup A B e' eq_f the_list' = None ….
1669	#A #B #e #e' #the_list elim the_list
1670	[1:
1671	#the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
1672	\|2:
1673	#hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
1674	whd in ⊢ (??%? → ??%?); <e_refl
1675	cases (eq_f (\fst hd) e) normalize nodelta
1676	[1:
1677	#absurd destruct(absurd)
1678	\|2:
1679	>e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
1680	]
1681	]
1682	qed.*)
1683
1684	lemma sfr_psw_eq_to_bit_address_of_register_eq:
1685	∀A: Type[0].
1686	∀code_memory: A.
1687	∀status, status', register_address.
1688	get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1689	bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
1690	#A #code_memory #status #status' #register_address #sfr_psw_refl
1691	whd in match bit_address_of_register; normalize nodelta
1692	<sfr_psw_refl %
1693	qed.
1694
1695	lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
1696	∀A: Type[0].
1697	∀code_memory: A.
1698	∀status, status', register_address.
1699	get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1700	low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
1701	get_register A code_memory status register_address = get_register A code_memory status' register_address.
1702	#A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
1703	whd in match get_register; normalize nodelta <low_internal_ram_refl
1704	>(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
1705	qed.
1706
1707	lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
1708	∀M, cm, status, status', sigma.
1709	∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
1710	get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1711	assert_data pseudo_assembly_program M cm status addr1 = true →
1712	map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1.
1713	* * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl
1714	@(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w
1715	whd in ⊢ (??%? → %); whd in match (data_or_address ?????);
1716	whd in match exists; normalize nodelta
1717	<(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption
1718	cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
1719	qed.
1720
1721	lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
1722	∀M.
1723	∀sigma.
1724	∀sfr8051.
1725	∀b.
1726	sfr8051 ≠ SFR_ACC_A →
1727	map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
1728	#M #sigma * #b
1729	[18:
1730	#relevant cases (absurd … (refl ??) relevant)
1731	]
1732	#_ %
1733	qed.
1734
1735	lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
1736	∀M.
1737	∀sigma: Word → Word.
1738	∀w: BitVector 8.
1739	∀b.
1740	w ≠ bitvector_of_nat … 224 →
1741	map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
1742	#M #sigma #w #b #w_neq_assm
1743	whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
1744	[1:
1745	#sfr_of_Byte_refl %
1746	\|2:
1747	* #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
1748	@sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
1749	#relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
1750	@(absurd ?? w_neq_assm)
1751	lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
1752	whd in match sfr_of_Byte; normalize nodelta
1753	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1754	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1755	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1756	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1757	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1758	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1759	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1760	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1761	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1762	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1763	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1764	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1765	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1766	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1767	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1768	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1769	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1770	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1771	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1772	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1773	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1774	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1775	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1776	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1777	@eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
1778	cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1779	#absurd destruct(absurd)
1780	qed.
1781
1782	(*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
1783	∀M, sigma, w, b.
1784	assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst M) = false →
1785	map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
1786	#M #sigma #w #b #assoc_list_exists_assm
1787	whd in ⊢ (??%?);
1788	>(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
1789	qed.*)
1790
1791	lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
1792	∀M', cm.
1793	∀sigma, status, status', b, b'.
1794	∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
1795	get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1796	low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
1797	b = b' →
1798	assert_data pseudo_assembly_program M' cm status addr1 = true →
1799	map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
1800	#M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
1801	@(subaddressing_mode_elim … addr1)
1802	[1:
1803	whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high *
1804	[1:
1805	normalize nodelta #_ %
1806	\|2:
1807	* #upper_lower #address normalize nodelta #absurd destruct(absurd)
1808	]
1809	\|2: cases M' -M' * #low #high #accA
1810	#w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??);
1811	<(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
1812	cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
1813	\|4: cases M' -M' * #low #high #accA
1814	#w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram;
1815	whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta
1816	whd in match get_register; normalize nodelta
1817	<(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl)
1818	cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)]
1819	<low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta
1820	cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta
1821	#x try % #abs destruct(abs)
1822	\|3: cases M' -M' * #low #high #accA
1823	#w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta
1824	@vsplit_elim #hd #tl #w_refl normalize nodelta
1825	lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd))
1826	cases (head' bool ??) normalize nodelta
1827	[2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????);
1828	whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????);
1829	normalize nodelta // #x #abs destruct(abs) ] #EQhd
1830	>w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta
1831	[1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_
1832	normalize in eq_bv_refl; >eq_bv_refl %
1833	\|2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ]
1834	\|5,6,7,8:
1835	#w try #w' %
1836	]
1837	qed.
1838
1839	(CSC: move elsewhere)
1840	lemma bv_append_eq_to_eq:
1841	∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
1842	v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
1843	#A #n #v1 elim v1
1844	[ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
1845	\| #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
1846	#m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
1847	qed.
1848
1849	lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
1850	∀M: internal_pseudo_address_map.
1851	∀cm: pseudo_assembly_program.
1852	∀s: PreStatus pseudo_assembly_program cm.
1853	∀sigma: Word → Word.
1854	∀addr: [[bit_addr]]. (* XXX: expand as needed *)
1855	∀f: bool.
1856	assert_data pseudo_assembly_program M cm s addr = true →
1857	map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
1858	** #low #high #accA #cm #s #sigma #addr #f
1859	@(subaddressing_mode_elim … addr) #w
1860	whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta
1861	@vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1862	@vsplit_elim #four #three #four_three_refl normalize nodelta
1863	cases (head' bool ??) normalize nodelta
1864	[1: @eq_bv_elim normalize nodelta
1865	[1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour %
1866	\|2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map
1867	try % normalize #EQ @(absurd ?? NEQ)
1868	cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1
1869	cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ]
1870	\|2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
1871	whd in match lookup_from_internal_ram; normalize nodelta
1872	cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ]
1873	qed.
1874
1875	(*
1876	lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
1877	∀M: internal_pseudo_address_map.
1878	∀cm: pseudo_assembly_program.
1879	∀s, s': PreStatus pseudo_assembly_program cm.
1880	∀sigma: Word → Word.
1881	∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
1882	∀f: bool.
1883	s = s' →
1884	addressing_mode_ok pseudo_assembly_program M cm s addr = true →
1885	map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
1886	#M #cm #s #s' #sigma #addr #f #s_refl <s_refl
1887	@(subaddressing_mode_elim … addr) [1: #w ]
1888	whd in ⊢ (??%? → %); [2: #_ @I ]
1889	inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1890	cases (head' bool ??) normalize nodelta
1891	[1:
1892	#eq_accumulator_assm whd in ⊢ (??%?);
1893	cases (sfr_of_Byte ?) try % * * try % normalize nodelta
1894	whd in ⊢ (??%?);
1895	>(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
1896	\|2:
1897	#assoc_list_exists_assm whd in ⊢ (??%?);
1898	lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
1899	whd in assoc_list_exists_assm:(???%);
1900	>(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
1901	]
1902	qed.
1903
1904	lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
1905	∀M: internal_pseudo_address_map.
1906	∀cm: pseudo_assembly_program.
1907	∀s, s': PreStatus pseudo_assembly_program cm.
1908	∀sigma: Word → Word.
1909	∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
1910	∀f: bool.
1911	s = s' →
1912	addressing_mode_ok pseudo_assembly_program M cm s addr = true →
1913	map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
1914	#M #cm #s #s' #sigma #addr #f #s_refl <s_refl
1915	@(subaddressing_mode_elim … addr) [1: #w ]
1916	whd in ⊢ (??%? → %); [2: #_ @I ]
1917	inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1918	cases (head' bool ??) normalize nodelta
1919	[1:
1920	#eq_accumulator_assm whd in ⊢ (??%?);
1921	cases (sfr_of_Byte ?) try % * * try % normalize nodelta
1922	whd in ⊢ (??%?);
1923	>(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
1924	\|2:
1925	#assoc_list_exists_assm whd in ⊢ (??%?);
1926	lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
1927	whd in assoc_list_exists_assm:(???%);
1928	>(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
1929	]
1930	qed.*)
1931
1932	(*
1933	axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
1934	∀M, M', sigma,cm,s,addr,v,v'.
1935	(∀addr'.
1936	((false:::addr) = addr' →
1937	map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
1938	map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
1939	((false:::addr) ≠ addr' →
1940	let 〈callM, accM〉 ≝ M in
1941	let 〈callM', accM'〉 ≝ M' in
1942	accM = accM' ∧
1943	assoc_list_lookup … addr' (eq_bv 8) … callM =
1944	assoc_list_lookup … addr' (eq_bv 8) … callM')) →
1945	insert Byte 7 addr v'
1946	(low_internal_ram_of_pseudo_low_internal_ram M'
1947	(low_internal_ram pseudo_assembly_program cm s)) =
1948	low_internal_ram_of_pseudo_low_internal_ram M
1949	(insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
1950	*)
1951
1952	(*
1953	lemma write_at_stack_pointer_status_of_pseudo_status:
1954	∀M, M'.
1955	∀cm.
1956	∀sigma.
1957	∀policy.
1958	∀s, s'.
1959	∀new_b, new_b'.
1960	map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
1961	status_of_pseudo_status M cm s sigma policy = s' →
1962	write_at_stack_pointer ?? s' new_b' =
1963	status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
1964	#M #M' #cm #sigma #policy #s #s' #new_b #new_b'
1965	#new_b_refl #s_refl <new_b_refl <s_refl
1966	whd in match write_at_stack_pointer; normalize nodelta
1967	@pair_elim #nu #nl #nu_nl_refl normalize nodelta
1968	@(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
1969	[1:
1970	@eq_f
1971	whd in match get_8051_sfr; normalize nodelta
1972	whd in match sfr_8051_index; normalize nodelta
1973	whd in match status_of_pseudo_status; normalize nodelta
1974	whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1975	cases (\snd M) [2: * #address ] normalize nodelta
1976	[1,2:
1977	cases (vsplit bool ???) #high #low normalize nodelta
1978	whd in match sfr_8051_index; normalize nodelta
1979	>get_index_v_set_index_miss %
1980	#absurd destruct(absurd)
1981	\|3:
1982	%
1983	]
1984	\|2:
1985	@if_then_else_status_of_pseudo_status try %
1986	[2:
1987	@sym_eq <set_low_internal_ram_status_of_pseudo_status
1988	[1:
1989	@eq_f2
1990	[2:
1991	@insert_low_internal_ram_of_pseudo_low_internal_ram'
1992	@sym_eq
1993	[2:
1994	<set_low_internal_ram_status_of_pseudo_status
1995	[1:
1996	@eq_f2
1997	[2:
1998	@sym_eq
1999	>(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
2000	[2:
2001	>new_b_refl
2002	]
2003	]
2004	qed.*)

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

Download in other formats:

Original Format