Context Navigation

Interpret.ma @ 1910

Last change on this file since 1910 was 1910, checked in by mulligan, 8 years ago
Finished proof modulo termination argument
File size: 48.0 KB

Line
1	include "ASM/StatusProofs.ma".
2	include "common/StructuredTraces.ma".
3	include "ASM/Fetch.ma".
4
5	definition sign_extension: Byte → Word ≝
6	λc.
7	let b ≝ get_index_v ? 8 c 1 ? in
8	[[ b; b; b; b; b; b; b; b ]] @@ c.
9	normalize;
10	repeat (@ (le_S_S ?));
11	@ (le_O_n);
12	qed.
13
14	lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
15	# a
16	# b
17	cases a
18	cases b
19	normalize
20	# K
21	try %
22	cases (eq_true_false K)
23	qed.
24
25	lemma is_a_to_mem_to_is_in:
26	∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
27	# he
28	# a
29	# m
30	# q
31	elim q
32	[ normalize
33	# _
34	# K
35	assumption
36	\| # m'
37	# t
38	# q'
39	# II
40	# H1
41	# H2
42	normalize
43	change with (orb ??) in H2: (??%?);
44	cases (inclusive_disjunction_true … H2)
45	[ # K
46	< (eq_a_to_eq … K)
47	> H1
48	%
49	\| # K
50	> II
51	try assumption
52	cases (is_a t a)
53	normalize
54	%
55	]
56	]
57	qed.
58
59	lemma execute_1_technical:
60	∀n, m: nat.
61	∀v: Vector addressing_mode_tag (S n).
62	∀q: Vector addressing_mode_tag (S m).
63	∀a: addressing_mode.
64	bool_to_Prop (is_in ? v a) →
65	bool_to_Prop (subvector_with ? ? ? eq_a v q) →
66	bool_to_Prop (is_in ? q a).
67	# n
68	# m
69	# v
70	# q
71	# a
72	elim v
73	[ normalize
74	# K
75	cases K
76	\| # n'
77	# he
78	# tl
79	# II
80	whd in ⊢ (% → ? → ?);
81	lapply (refl … (is_in … (he:::tl) a))
82	cases (is_in … (he:::tl) a) in ⊢ (???% → %);
83	[ # K
84	# _
85	normalize in K;
86	whd in ⊢ (% → ?);
87	lapply (refl … (subvector_with … eq_a (he:::tl) q));
88	cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
89	[ # K1
90	# _
91	change with ((andb ? (subvector_with …)) = true) in K1;
92	cases (conjunction_true … K1)
93	# K3
94	# K4
95	cases (inclusive_disjunction_true … K)
96	# K2
97	[ > (is_a_to_mem_to_is_in … K2 K3)
98	%
99	\| @ II
100	[ > K2
101	%
102	\| > K4
103	%
104	]
105	]
106	\| # K1
107	# K2
108	normalize in K2;
109	cases K2;
110	]
111	\| # K1
112	# K2
113	normalize in K2;
114	cases K2
115	]
116	]
117	qed.
118
119	include alias "arithmetics/nat.ma".
120	include alias "ASM/BitVectorTrie.ma".
121
122	definition ASM_classify00: ∀a. preinstruction a → status_class ≝
123	λa, pre.
124	match pre with
125	[ RET ⇒ cl_return
126	\| RETI ⇒ cl_return
127	\| JZ _ ⇒ cl_jump
128	\| JNZ _ ⇒ cl_jump
129	\| JC _ ⇒ cl_jump
130	\| JNC _ ⇒ cl_jump
131	\| JB _ _ ⇒ cl_jump
132	\| JNB _ _ ⇒ cl_jump
133	\| JBC _ _ ⇒ cl_jump
134	\| CJNE _ _ ⇒ cl_jump
135	\| DJNZ _ _ ⇒ cl_jump
136	\| _ ⇒ cl_other
137	].
138
139	definition ASM_classify0: instruction → status_class ≝
140	λi.
141	match i with
142	[ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
143	\| ACALL _ ⇒ cl_call
144	\| LCALL _ ⇒ cl_call
145	\| JMP _ ⇒ cl_call
146	\| AJMP _ ⇒ cl_other
147	\| LJMP _ ⇒ cl_other
148	\| SJMP _ ⇒ cl_other
149	\| _ ⇒ cl_other
150	].
151
152	definition current_instruction0 ≝
153	λcode_memory: BitVectorTrie Byte 16.
154	λprogram_counter: Word.
155	\fst (\fst (fetch … code_memory program_counter)).
156
157	definition current_instruction ≝
158	λcode_memory.
159	λs: Status code_memory.
160	current_instruction0 code_memory (program_counter … s).
161
162	definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
163	λcode_memory.
164	λs: Status code_memory.
165	ASM_classify0 (current_instruction … s).
166
167	definition execute_1_preinstruction':
168	∀ticks: nat × nat.
169	∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
170	∀s: PreStatus m cm.
171	Σs': PreStatus m cm.
172	And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
173	(ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
174	λticks: nat × nat.
175	λa, m: Type[0]. λcm.
176	λaddr_of: a → PreStatus m cm → Word.
177	λinstr: preinstruction a.
178	λs: PreStatus m cm.
179	let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
180	let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
181	match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
182	And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
183	(ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with
184	[ ADD addr1 addr2 ⇒ λinstr_refl.
185	let s ≝ add_ticks1 s in
186	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
187	(get_arg_8 … s false addr2) false in
188	let cy_flag ≝ get_index' ? O ? flags in
189	let ac_flag ≝ get_index' ? 1 ? flags in
190	let ov_flag ≝ get_index' ? 2 ? flags in
191	let s ≝ set_arg_8 … s ACC_A result in
192	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
193	\| ADDC addr1 addr2 ⇒ λinstr_refl.
194	let s ≝ add_ticks1 s in
195	let old_cy_flag ≝ get_cy_flag ?? s in
196	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
197	(get_arg_8 … s false addr2) old_cy_flag in
198	let cy_flag ≝ get_index' ? O ? flags in
199	let ac_flag ≝ get_index' ? 1 ? flags in
200	let ov_flag ≝ get_index' ? 2 ? flags in
201	let s ≝ set_arg_8 … s ACC_A result in
202	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
203	\| SUBB addr1 addr2 ⇒ λinstr_refl.
204	let s ≝ add_ticks1 s in
205	let old_cy_flag ≝ get_cy_flag ?? s in
206	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
207	(get_arg_8 … s false addr2) old_cy_flag in
208	let cy_flag ≝ get_index' ? O ? flags in
209	let ac_flag ≝ get_index' ? 1 ? flags in
210	let ov_flag ≝ get_index' ? 2 ? flags in
211	let s ≝ set_arg_8 … s ACC_A result in
212	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
213	\| ANL addr ⇒ λinstr_refl.
214	let s ≝ add_ticks1 s in
215	match addr with
216	[ inl l ⇒
217	match l with
218	[ inl l' ⇒
219	let 〈addr1, addr2〉 ≝ l' in
220	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
221	set_arg_8 … s addr1 and_val
222	\| inr r ⇒
223	let 〈addr1, addr2〉 ≝ r in
224	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
225	set_arg_8 … s addr1 and_val
226	]
227	\| inr r ⇒
228	let 〈addr1, addr2〉 ≝ r in
229	let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
230	set_flags … s and_val (None ?) (get_ov_flag ?? s)
231	]
232	\| ORL addr ⇒ λinstr_refl.
233	let s ≝ add_ticks1 s in
234	match addr with
235	[ inl l ⇒
236	match l with
237	[ inl l' ⇒
238	let 〈addr1, addr2〉 ≝ l' in
239	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
240	set_arg_8 … s addr1 or_val
241	\| inr r ⇒
242	let 〈addr1, addr2〉 ≝ r in
243	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
244	set_arg_8 … s addr1 or_val
245	]
246	\| inr r ⇒
247	let 〈addr1, addr2〉 ≝ r in
248	let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
249	set_flags … s or_val (None ?) (get_ov_flag … s)
250	]
251	\| XRL addr ⇒ λinstr_refl.
252	let s ≝ add_ticks1 s in
253	match addr with
254	[ inl l' ⇒
255	let 〈addr1, addr2〉 ≝ l' in
256	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
257	set_arg_8 … s addr1 xor_val
258	\| inr r ⇒
259	let 〈addr1, addr2〉 ≝ r in
260	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
261	set_arg_8 … s addr1 xor_val
262	]
263	\| INC addr ⇒ λinstr_refl.
264	match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
265	[ ACC_A ⇒ λacc_a: True.
266	let s' ≝ add_ticks1 s in
267	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
268	set_arg_8 … s' ACC_A result
269	\| REGISTER r ⇒ λregister: True.
270	let s' ≝ add_ticks1 s in
271	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
272	set_arg_8 … s' (REGISTER r) result
273	\| DIRECT d ⇒ λdirect: True.
274	let s' ≝ add_ticks1 s in
275	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
276	set_arg_8 … s' (DIRECT d) result
277	\| INDIRECT i ⇒ λindirect: True.
278	let s' ≝ add_ticks1 s in
279	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
280	set_arg_8 … s' (INDIRECT i) result
281	\| DPTR ⇒ λdptr: True.
282	let s' ≝ add_ticks1 s in
283	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
284	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
285	let s ≝ set_8051_sfr … s' SFR_DPL bl in
286	set_8051_sfr … s' SFR_DPH bu
287	\| _ ⇒ λother: False. ⊥
288	] (subaddressing_modein … addr)
289	\| NOP ⇒ λinstr_refl.
290	let s ≝ add_ticks2 s in
291	s
292	\| DEC addr ⇒ λinstr_refl.
293	let s ≝ add_ticks1 s in
294	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
295	set_arg_8 … s addr result
296	\| MUL addr1 addr2 ⇒ λinstr_refl.
297	let s ≝ add_ticks1 s in
298	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
299	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
300	let product ≝ acc_a_nat * acc_b_nat in
301	let ov_flag ≝ product ≥ 256 in
302	let low ≝ bitvector_of_nat 8 (product mod 256) in
303	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
304	let s ≝ set_8051_sfr … s SFR_ACC_A low in
305	set_8051_sfr … s SFR_ACC_B high
306	\| DIV addr1 addr2 ⇒ λinstr_refl.
307	let s ≝ add_ticks1 s in
308	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
309	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
310	match acc_b_nat with
311	[ O ⇒ set_flags … s false (None Bit) true
312	\| S o ⇒
313	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
314	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
315	let s ≝ set_8051_sfr … s SFR_ACC_A q in
316	let s ≝ set_8051_sfr … s SFR_ACC_B r in
317	set_flags … s false (None Bit) false
318	]
319	\| DA addr ⇒ λinstr_refl.
320	let s ≝ add_ticks1 s in
321	let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
322	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
323	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
324	let cy_flag ≝ get_index' ? O ? flags in
325	let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
326	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
327	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
328	let new_acc ≝ nu @@ acc_nl' in
329	let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
330	set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
331	else
332	s
333	else
334	s
335	\| CLR addr ⇒ λinstr_refl.
336	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
337	[ ACC_A ⇒ λacc_a: True.
338	let s ≝ add_ticks1 s in
339	set_arg_8 … s ACC_A (zero 8)
340	\| CARRY ⇒ λcarry: True.
341	let s ≝ add_ticks1 s in
342	set_arg_1 … s CARRY false
343	\| BIT_ADDR b ⇒ λbit_addr: True.
344	let s ≝ add_ticks1 s in
345	set_arg_1 … s (BIT_ADDR b) false
346	\| _ ⇒ λother: False. ⊥
347	] (subaddressing_modein … addr)
348	\| CPL addr ⇒ λinstr_refl.
349	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
350	[ ACC_A ⇒ λacc_a: True.
351	let s ≝ add_ticks1 s in
352	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
353	let new_acc ≝ negation_bv ? old_acc in
354	set_8051_sfr … s SFR_ACC_A new_acc
355	\| CARRY ⇒ λcarry: True.
356	let s ≝ add_ticks1 s in
357	let old_cy_flag ≝ get_arg_1 … s CARRY true in
358	let new_cy_flag ≝ ¬old_cy_flag in
359	set_arg_1 … s CARRY new_cy_flag
360	\| BIT_ADDR b ⇒ λbit_addr: True.
361	let s ≝ add_ticks1 s in
362	let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
363	let new_bit ≝ ¬old_bit in
364	set_arg_1 … s (BIT_ADDR b) new_bit
365	\| _ ⇒ λother: False. ?
366	] (subaddressing_modein … addr)
367	\| SETB b ⇒ λinstr_refl.
368	let s ≝ add_ticks1 s in
369	set_arg_1 … s b false
370	\| RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
371	let s ≝ add_ticks1 s in
372	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
373	let new_acc ≝ rotate_left … 1 old_acc in
374	set_8051_sfr … s SFR_ACC_A new_acc
375	\| RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
376	let s ≝ add_ticks1 s in
377	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
378	let new_acc ≝ rotate_right … 1 old_acc in
379	set_8051_sfr … s SFR_ACC_A new_acc
380	\| RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
381	let s ≝ add_ticks1 s in
382	let old_cy_flag ≝ get_cy_flag ?? s in
383	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
384	let new_cy_flag ≝ get_index' ? O ? old_acc in
385	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
386	let s ≝ set_arg_1 … s CARRY new_cy_flag in
387	set_8051_sfr … s SFR_ACC_A new_acc
388	\| RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
389	let s ≝ add_ticks1 s in
390	let old_cy_flag ≝ get_cy_flag ?? s in
391	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
392	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
393	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
394	let s ≝ set_arg_1 … s CARRY new_cy_flag in
395	set_8051_sfr … s SFR_ACC_A new_acc
396	\| SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
397	let s ≝ add_ticks1 s in
398	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
399	let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
400	let new_acc ≝ nl @@ nu in
401	set_8051_sfr … s SFR_ACC_A new_acc
402	\| PUSH addr ⇒ λinstr_refl.
403	match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
404	[ DIRECT d ⇒ λdirect: True.
405	let s ≝ add_ticks1 s in
406	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
407	let s ≝ set_8051_sfr … s SFR_SP new_sp in
408	write_at_stack_pointer … s d
409	\| _ ⇒ λother: False. ⊥
410	] (subaddressing_modein … addr)
411	\| POP addr ⇒ λinstr_refl.
412	let s ≝ add_ticks1 s in
413	let contents ≝ read_at_stack_pointer ?? s in
414	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
415	let s ≝ set_8051_sfr … s SFR_SP new_sp in
416	set_arg_8 … s addr contents
417	\| XCH addr1 addr2 ⇒ λinstr_refl.
418	let s ≝ add_ticks1 s in
419	let old_addr ≝ get_arg_8 … s false addr2 in
420	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
421	let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
422	set_arg_8 … s addr2 old_acc
423	\| XCHD addr1 addr2 ⇒ λinstr_refl.
424	let s ≝ add_ticks1 s in
425	let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
426	let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
427	let new_acc ≝ acc_nu @@ arg_nl in
428	let new_arg ≝ arg_nu @@ acc_nl in
429	let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
430	set_arg_8 … s addr2 new_arg
431	\| RET ⇒ λinstr_refl.
432	let s ≝ add_ticks1 s in
433	let high_bits ≝ read_at_stack_pointer ?? s in
434	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
435	let s ≝ set_8051_sfr … s SFR_SP new_sp in
436	let low_bits ≝ read_at_stack_pointer ?? s in
437	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
438	let s ≝ set_8051_sfr … s SFR_SP new_sp in
439	let new_pc ≝ high_bits @@ low_bits in
440	set_program_counter … s new_pc
441	\| RETI ⇒ λinstr_refl.
442	let s ≝ add_ticks1 s in
443	let high_bits ≝ read_at_stack_pointer ?? s in
444	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
445	let s ≝ set_8051_sfr … s SFR_SP new_sp in
446	let low_bits ≝ read_at_stack_pointer ?? s in
447	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
448	let s ≝ set_8051_sfr … s SFR_SP new_sp in
449	let new_pc ≝ high_bits @@ low_bits in
450	set_program_counter … s new_pc
451	\| MOVX addr ⇒ λinstr_refl.
452	let s ≝ add_ticks1 s in
453	(* DPM: only copies --- doesn't affect I/O *)
454	match addr with
455	[ inl l ⇒
456	let 〈addr1, addr2〉 ≝ l in
457	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
458	\| inr r ⇒
459	let 〈addr1, addr2〉 ≝ r in
460	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
461	]
462	\| MOV addr ⇒ λinstr_refl.
463	let s ≝ add_ticks1 s in
464	match addr with
465	[ inl l ⇒
466	match l with
467	[ inl l' ⇒
468	match l' with
469	[ inl l'' ⇒
470	match l'' with
471	[ inl l''' ⇒
472	match l''' with
473	[ inl l'''' ⇒
474	let 〈addr1, addr2〉 ≝ l'''' in
475	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
476	\| inr r'''' ⇒
477	let 〈addr1, addr2〉 ≝ r'''' in
478	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
479	]
480	\| inr r''' ⇒
481	let 〈addr1, addr2〉 ≝ r''' in
482	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
483	]
484	\| inr r'' ⇒
485	let 〈addr1, addr2〉 ≝ r'' in
486	set_arg_16 … s (get_arg_16 … s addr2) addr1
487	]
488	\| inr r ⇒
489	let 〈addr1, addr2〉 ≝ r in
490	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
491	]
492	\| inr r ⇒
493	let 〈addr1, addr2〉 ≝ r in
494	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
495	]
496	\| JC addr ⇒ λinstr_refl.
497	if get_cy_flag ?? s then
498	let s ≝ add_ticks1 s in
499	set_program_counter … s (addr_of addr s)
500	else
501	let s ≝ add_ticks2 s in
502	s
503	\| JNC addr ⇒ λinstr_refl.
504	if ¬(get_cy_flag ?? s) then
505	let s ≝ add_ticks1 s in
506	set_program_counter … s (addr_of addr s)
507	else
508	let s ≝ add_ticks2 s in
509	s
510	\| JB addr1 addr2 ⇒ λinstr_refl.
511	if get_arg_1 … s addr1 false then
512	let s ≝ add_ticks1 s in
513	set_program_counter … s (addr_of addr2 s)
514	else
515	let s ≝ add_ticks2 s in
516	s
517	\| JNB addr1 addr2 ⇒ λinstr_refl.
518	if ¬(get_arg_1 … s addr1 false) then
519	let s ≝ add_ticks1 s in
520	set_program_counter … s (addr_of addr2 s)
521	else
522	let s ≝ add_ticks2 s in
523	s
524	\| JBC addr1 addr2 ⇒ λinstr_refl.
525	let s ≝ set_arg_1 … s addr1 false in
526	if get_arg_1 … s addr1 false then
527	let s ≝ add_ticks1 s in
528	set_program_counter … s (addr_of addr2 s)
529	else
530	let s ≝ add_ticks2 s in
531	s
532	\| JZ addr ⇒ λinstr_refl.
533	if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
534	let s ≝ add_ticks1 s in
535	set_program_counter … s (addr_of addr s)
536	else
537	let s ≝ add_ticks2 s in
538	s
539	\| JNZ addr ⇒ λinstr_refl.
540	if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
541	let s ≝ add_ticks1 s in
542	set_program_counter … s (addr_of addr s)
543	else
544	let s ≝ add_ticks2 s in
545	s
546	\| CJNE addr1 addr2 ⇒ λinstr_refl.
547	match addr1 with
548	[ inl l ⇒
549	let 〈addr1, addr2'〉 ≝ l in
550	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
551	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
552	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
553	let s ≝ add_ticks1 s in
554	let s ≝ set_program_counter … s (addr_of addr2 s) in
555	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
556	else
557	let s ≝ add_ticks2 s in
558	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
559	\| inr r' ⇒
560	let 〈addr1, addr2'〉 ≝ r' in
561	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
562	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
563	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
564	let s ≝ add_ticks1 s in
565	let s ≝ set_program_counter … s (addr_of addr2 s) in
566	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
567	else
568	let s ≝ add_ticks2 s in
569	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
570	]
571	\| DJNZ addr1 addr2 ⇒ λinstr_refl.
572	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
573	let s ≝ set_arg_8 … s addr1 result in
574	if ¬(eq_bv ? result (zero 8)) then
575	let s ≝ add_ticks1 s in
576	set_program_counter … s (addr_of addr2 s)
577	else
578	let s ≝ add_ticks2 s in
579	s
580	] (refl … instr).
581	try (cases(other))
582	try assumption (20s)
583	try (% @False) (6s) (* Bug exploited here to implement solve :-*)
584	try (
585	@(execute_1_technical … (subaddressing_modein …))
586	@I
587	) (66s)
588	normalize nodelta %
589	try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
590	try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd))
591	try (@or_introl //)
592	try (@or_intror //)
593	#_ /demod/ %
594	qed.
595
596	definition execute_1_preinstruction:
597	∀ticks: nat × nat.
598	∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
599	PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
600
601	lemma execute_1_preinstruction_ok:
602	∀ticks,a,m,cm,f,i,s.
603	(clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
604	clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
605	(ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
606	#ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
607	qed.
608
609	discriminator Prod.
610
611	definition compute_target_of_unconditional_jump:
612	∀program_counter: Word.
613	∀i: instruction.
614	Word ≝
615	λprogram_counter.
616	λi.
617	match i with
618	[ LJMP addr ⇒
619	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
620	[ ADDR16 a ⇒ λaddr16: True. a
621	\| _ ⇒ λother: False. ⊥
622	] (subaddressing_modein … addr)
623	\| SJMP addr ⇒
624	match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
625	[ RELATIVE r ⇒ λrelative: True.
626	let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
627	new_pc
628	\| _ ⇒ λother: False. ⊥
629	] (subaddressing_modein … addr)
630	\| AJMP addr ⇒
631	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
632	[ ADDR11 a ⇒ λaddr11: True.
633	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
634	let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
635	let bit ≝ get_index' ? O ? nl in
636	let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
637	let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
638	let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
639	new_pc
640	\| _ ⇒ λother: False. ⊥
641	] (subaddressing_modein … addr)
642	\| _ ⇒ zero ?
643	].
644	//
645	qed.
646
647	definition is_unconditional_jump:
648	instruction → bool ≝
649	λi: instruction.
650	match i with
651	[ LJMP _ ⇒ true
652	\| SJMP _ ⇒ true
653	\| AJMP _ ⇒ true
654	\| _ ⇒ false
655	].
656
657	let rec member_addressing_mode_tag
658	(n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
659	on v: Prop ≝
660	match v with
661	[ VEmpty ⇒ False
662	\| VCons n' hd tl ⇒
663	bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
664	].
665
666	lemma is_a_decidable:
667	∀hd.
668	∀element.
669	is_a hd element = true ∨ is_a hd element = false.
670	#hd #element //
671	qed.
672
673	lemma mem_decidable:
674	∀n: nat.
675	∀v: Vector addressing_mode_tag n.
676	∀element: addressing_mode_tag.
677	mem … eq_a n v element = true ∨
678	mem … eq_a … v element = false.
679	#n #v #element //
680	qed.
681
682	lemma eq_a_elim:
683	∀tag.
684	∀hd.
685	∀P: bool → Prop.
686	(tag = hd → P (true)) →
687	(tag ≠ hd → P (false)) →
688	P (eq_a tag hd).
689	#tag #hd #P
690	cases tag
691	cases hd
692	#true_hyp #false_hyp
693	try @false_hyp
694	try @true_hyp
695	try %
696	#absurd destruct(absurd)
697	qed.
698
699	lemma is_a_true_to_is_in:
700	∀n: nat.
701	∀x: addressing_mode.
702	∀tag: addressing_mode_tag.
703	∀supervector: Vector addressing_mode_tag n.
704	mem addressing_mode_tag eq_a n supervector tag →
705	is_a tag x = true →
706	is_in … supervector x.
707	#n #x #tag #supervector
708	elim supervector
709	[1:
710	#absurd cases absurd
711	\|2:
712	#n' #hd #tl #inductive_hypothesis
713	whd in match (mem … eq_a (S n') (hd:::tl) tag);
714	@eq_a_elim normalize nodelta
715	[1:
716	#tag_hd_eq #irrelevant
717	whd in match (is_in (S n') (hd:::tl) x);
718	<tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
719	@I
720	\|2:
721	#tag_hd_neq
722	whd in match (is_in (S n') (hd:::tl) x);
723	change with (
724	mem … eq_a n' tl tag)
725	in match (fold_right … n' ? false tl);
726	#mem_hyp #is_a_hyp
727	cases(is_a hd x)
728	[1:
729	normalize nodelta //
730	\|2:
731	normalize nodelta
732	@inductive_hypothesis assumption
733	]
734	]
735	]
736	qed.
737
738	lemma is_in_subvector_is_in_supervector:
739	∀m, n: nat.
740	∀subvector: Vector addressing_mode_tag m.
741	∀supervector: Vector addressing_mode_tag n.
742	∀element: addressing_mode.
743	subvector_with … eq_a subvector supervector →
744	is_in m subvector element → is_in n supervector element.
745	#m #n #subvector #supervector #element
746	elim subvector
747	[1:
748	#subvector_with_proof #is_in_proof
749	cases is_in_proof
750	\|2:
751	#n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
752	whd in match (is_in … (hd':::tl') element);
753	cases (is_a_decidable hd' element)
754	[1:
755	#is_a_true >is_a_true
756	#irrelevant
757	whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
758	@(is_a_true_to_is_in … is_a_true)
759	lapply(subvector_with_proof)
760	cases(mem … eq_a n supervector hd') //
761	\|2:
762	#is_a_false >is_a_false normalize nodelta
763	#assm
764	@inductive_hypothesis
765	[1:
766	generalize in match subvector_with_proof;
767	whd in match (subvector_with … eq_a (hd':::tl') supervector);
768	cases(mem_decidable n supervector hd')
769	[1:
770	#mem_true >mem_true normalize nodelta
771	#assm assumption
772	\|2:
773	#mem_false >mem_false #absurd
774	cases absurd
775	]
776	\|2:
777	assumption
778	]
779	]
780	]
781	qed.
782
783	let rec subaddressing_mode_elim_type
784	(T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
785	(Q: addressing_mode → T → Prop)
786	(p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T)
787	(p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T)
788	(p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T)
789	(p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T)
790	(p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T)
791	(p_acc_a: is_in m fixed_v ACC_A → T)
792	(p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T)
793	(p_acc_b: is_in m fixed_v ACC_B → T)
794	(p_dptr: is_in m fixed_v DPTR → T)
795	(p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T)
796	(p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T)
797	(p_acc_dptr: is_in m fixed_v ACC_DPTR → T)
798	(p_acc_pc: is_in m fixed_v ACC_PC → T)
799	(p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T)
800	(p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T)
801	(p_carry: is_in m fixed_v CARRY → T)
802	(p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T)
803	(p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T)
804	(p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T)
805	(n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
806	on v: Prop ≝
807	match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
808	[ VEmpty ⇒ λm_refl. λv_refl.
809	∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
810	Q addr (
811	match addr return λx: addressing_mode. is_in … fixed_v x → T with
812	[ ADDR11 x ⇒ p_addr11 x
813	\| ADDR16 x ⇒ p_addr16 x
814	\| DIRECT x ⇒ p_direct x
815	\| INDIRECT x ⇒ p_indirect x
816	\| EXT_INDIRECT x ⇒ p_ext_indirect x
817	\| ACC_A ⇒ p_acc_a
818	\| REGISTER x ⇒ p_register x
819	\| ACC_B ⇒ p_acc_b
820	\| DPTR ⇒ p_dptr
821	\| DATA x ⇒ p_data x
822	\| DATA16 x ⇒ p_data16 x
823	\| ACC_DPTR ⇒ p_acc_dptr
824	\| ACC_PC ⇒ p_acc_pc
825	\| EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
826	\| INDIRECT_DPTR ⇒ p_indirect_dptr
827	\| CARRY ⇒ p_carry
828	\| BIT_ADDR x ⇒ p_bit_addr x
829	\| N_BIT_ADDR x ⇒ p_n_bit_addr x
830	\| RELATIVE x ⇒ p_relative x
831	] p)
832	\| VCons n' hd tl ⇒ λm_refl. λv_refl.
833	let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
834	p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
835	p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
836	p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
837	p_bit_addr p_n_bit_addr p_relative n' tl ?
838	in
839	match hd return λa: addressing_mode_tag. a = hd → ? with
840	[ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
841	\| addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
842	\| direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
843	\| indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
844	\| ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
845	\| acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
846	\| registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
847	\| acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
848	\| dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
849	\| data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
850	\| data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
851	\| acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
852	\| acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
853	\| ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
854	\| indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
855	\| carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
856	\| bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
857	\| n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
858	\| relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
859	] (refl … hd)
860	] (refl … n) (refl_jmeq … v).
861	[20:
862	generalize in match proof; destruct
863	whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
864	cases (mem … eq_a m fixed_v hd) normalize nodelta
865	[1:
866	whd in match (subvector_with … eq_a tl fixed_v);
867	#assm assumption
868	\|2:
869	normalize in ⊢ (% → ?);
870	#absurd cases absurd
871	]
872	]
873	@(is_in_subvector_is_in_supervector … proof)
874	destruct @I
875	qed.
876
877	(* XXX: todo *)
878	lemma subaddressing_mode_elim':
879	∀T: Type[2].
880	∀n: nat.
881	∀o: nat.
882	∀v1: Vector addressing_mode_tag n.
883	∀v2: Vector addressing_mode_tag o.
884	∀Q: addressing_mode → T → Prop.
885	∀fixed_v: Vector addressing_mode_tag (n + o).
886	∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
887	∀fixed_v_proof: fixed_v = v1 @@ v2.
888	∀subaddressing_mode_proof.
889	subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
890	P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
891	#T #n #o #v1 #v2
892	elim v1 cases v2
893	[1:
894	#Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
895	#P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
896	#subaddressing_mode_proof destruct normalize
897	#addr #absurd cases absurd
898	\|2:
899	#n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
900	#P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
901	destruct normalize in match ([[]]@@hd:::tl);
902	]
903	cases daemon
904	qed.
905
906	(* XXX: todo *)
907	lemma subaddressing_mode_elim:
908	∀T: Type[2].
909	∀m: nat.
910	∀n: nat.
911	∀Q: addressing_mode → T → Prop.
912	∀fixed_v: Vector addressing_mode_tag m.
913	∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
914	∀v: Vector addressing_mode_tag n.
915	∀proof.
916	subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
917	P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
918	#T #m #n #Q #fixed_v
919	elim fixed_v
920	[1:
921	#P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
922	#P14 #P15 #P16 #P17 #P18 #P19 #v #proof
923	normalize
924	\|2:
925	]
926	cases daemon
927	qed.
928
929	definition program_counter_after_other ≝
930	λprogram_counter. (* XXX: program counter after fetching *)
931	λinstruction.
932	if is_unconditional_jump instruction then
933	compute_target_of_unconditional_jump program_counter instruction
934	else
935	program_counter.
936
937	definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
938	Σs': Status cm.
939	And (clock ?? s' = \snd current + clock … s)
940	(ASM_classify0 (\fst (\fst current)) = cl_other →
941	program_counter ? ? s' =
942	program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
943	λcm,s0,instr_pc_ticks.
944	let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
945	let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
946	let s ≝ set_program_counter … s0 pc in
947	match instr return λx. x = instr → Σs:?.? with
948	[ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
949	(λx. λs.
950	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
951	[ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
952	\| _ ⇒ λabsd. ⊥
953	] (subaddressing_modein … x)) instr' s
954	\| MOVC addr1 addr2 ⇒ λinstr_refl.
955	let s ≝ set_clock ?? s (ticks + clock … s) in
956	match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
957	[ ACC_DPTR ⇒ λacc_dptr: True.
958	let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
959	let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
960	let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
961	let result ≝ lookup ? ? new_addr cm (zero ?) in
962	set_8051_sfr … s SFR_ACC_A result
963	\| ACC_PC ⇒ λacc_pc: True.
964	let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
965	(* DPM: Under specified: does the carry from PC incrementation affect the *)
966	(* addition of the PC with the DPTR? At the moment, no. *)
967	let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
968	let result ≝ lookup ? ? new_addr cm (zero ?) in
969	set_8051_sfr … s SFR_ACC_A result
970	\| _ ⇒ λother: False. ⊥
971	] (subaddressing_modein … addr2)
972	\| JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
973	let s ≝ set_clock ?? s (ticks + clock … s) in
974	let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
975	let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
976	let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
977	let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
978	set_program_counter … s new_pc
979	\| LJMP addr ⇒ λinstr_refl.
980	let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
981	let s ≝ set_clock ?? s (ticks + clock … s) in
982	set_program_counter … s new_pc
983	\| SJMP addr ⇒ λinstr_refl.
984	let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
985	let s ≝ set_clock ?? s (ticks + clock … s) in
986	set_program_counter … s new_pc
987	\| AJMP addr ⇒ λinstr_refl.
988	let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
989	let s ≝ set_clock ?? s (ticks + clock … s) in
990	set_program_counter … s new_pc
991	\| ACALL addr ⇒ λinstr_refl.
992	let s ≝ set_clock ?? s (ticks + clock … s) in
993	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
994	[ ADDR11 a ⇒ λaddr11: True.
995	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
996	let s ≝ set_8051_sfr … s SFR_SP new_sp in
997	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
998	let s ≝ write_at_stack_pointer … s pc_bl in
999	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1000	let s ≝ set_8051_sfr … s SFR_SP new_sp in
1001	let s ≝ write_at_stack_pointer … s pc_bu in
1002	let 〈thr, eig〉 ≝ split ? 3 8 a in
1003	let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
1004	let new_addr ≝ (fiv @@ thr) @@ pc_bl in
1005	set_program_counter … s new_addr
1006	\| _ ⇒ λother: False. ⊥
1007	] (subaddressing_modein … addr)
1008	\| LCALL addr ⇒ λinstr_refl.
1009	let s ≝ set_clock ?? s (ticks + clock … s) in
1010	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
1011	[ ADDR16 a ⇒ λaddr16: True.
1012	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1013	let s ≝ set_8051_sfr … s SFR_SP new_sp in
1014	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
1015	let s ≝ write_at_stack_pointer … s pc_bl in
1016	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1017	let s ≝ set_8051_sfr … s SFR_SP new_sp in
1018	let s ≝ write_at_stack_pointer … s pc_bu in
1019	set_program_counter … s a
1020	\| _ ⇒ λother: False. ⊥
1021	] (subaddressing_modein … addr)
1022	] (refl … instr). (10s)
1023	try assumption
1024	[1,2,3,4,5,6,7,8:
1025	normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
1026	try //
1027	destruct(INSTR_PC) <instr_refl whd
1028	try (#absurd normalize in absurd; try destruct(absurd) try %) %
1029	\|9:
1030	cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
1031	(λx. λs.
1032	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1033	[ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
1034	\| _ ⇒ λabsd. ⊥
1035	] (subaddressing_modein … x)) instr' s) try @absd
1036	#clock_proof #classify_proof %
1037	[1:
1038	cases clock_proof #clock_proof' >clock_proof'
1039	destruct(INSTR_PC_TICKS) %
1040	\|2:
1041	-clock_proof <INSTR_PC_TICKS normalize nodelta
1042	cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
1043	[1:
1044	destruct(INSTR_PC) /2/
1045	\|2:
1046	* #hyp1 #hyp2 >hyp1 normalize nodelta
1047	<instr_refl normalize nodelta #hyp >classify_proof -classify_proof
1048	try assumption >hyp2 %
1049	]
1050	]
1051	qed.
1052
1053	definition current_instruction_cost ≝
1054	λcm.λs: Status cm.
1055	\snd (fetch cm (program_counter … s)).
1056
1057	definition execute_1': ∀cm.∀s:Status cm.
1058	Σs':Status cm.
1059	let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1060	And (clock ?? s' = current_instruction_cost cm s + clock … s)
1061	(ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1062	program_counter ? ? s' =
1063	program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
1064	λcm. λs: Status cm.
1065	let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1066	pi1 ?? (execute_1_0 cm s instr_pc_ticks).
1067	%
1068	[1:
1069	cases(execute_1_0 cm s instr_pc_ticks)
1070	#the_status * #clock_assm #_ @clock_assm
1071	\|2:
1072	cases(execute_1_0 cm s instr_pc_ticks)
1073	#the_status * #_ #classify_assm
1074	assumption
1075	]
1076	qed.
1077
1078	definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
1079
1080	lemma execute_1_ok: ∀cm.∀s.
1081	let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1082	(clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
1083	(ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1084	program_counter ? cm (execute_1 cm s) =
1085	program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
1086	(* (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
1087	#cm #s normalize nodelta
1088	whd in match execute_1; normalize nodelta @pi2
1089	qed-. (x Andrea: indexing takes ages here )
1090
1091	definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
1092	λticks,cm,s,instr,pc.
1093	let s ≝ set_program_counter ?? s pc in
1094	let s ≝
1095	match instr with
1096	[ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
1097	\| Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
1098	\| Cost cst ⇒ s
1099	\| Jmp jmp ⇒
1100	let s ≝ set_clock … s (\fst ticks + clock … s) in
1101	set_program_counter … s (address_of_word_labels cm jmp)
1102	\| Call call ⇒
1103	let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1104	let a ≝ address_of_word_labels cm call in
1105	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1106	let s ≝ set_8051_sfr … s SFR_SP new_sp in
1107	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
1108	let s ≝ write_at_stack_pointer … s pc_bl in
1109	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1110	let s ≝ set_8051_sfr … s SFR_SP new_sp in
1111	let s ≝ write_at_stack_pointer … s pc_bu in
1112	set_program_counter … s a
1113	\| Mov dptr ident ⇒
1114	let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1115	let the_preamble ≝ \fst cm in
1116	let data_labels ≝ construct_datalabels the_preamble in
1117	set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
1118	]
1119	in
1120	s.
1121	normalize
1122	@I
1123	qed.
1124
1125	definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
1126	λticks_of,cm,s.
1127	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
1128	let ticks ≝ ticks_of (program_counter … s) in
1129	execute_1_pseudo_instruction0 ticks cm s instr pc.
1130
1131	let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
1132	match n with
1133	[ O ⇒ s
1134	\| S o ⇒ execute o … (execute_1 … s)
1135	].
1136
1137	let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
1138	match n with
1139	[ O ⇒ s
1140	\| S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
1141	].

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

Download in other formats:

Original Format