Context Navigation

Interpret.ma @ 844

Last change on this file since 844 was 843, checked in by sacerdot, 10 years ago
Function moved from Interpret to Status.
File size: 28.7 KB

Line
1	include "ASM/Status.ma".
2	include "ASM/Fetch.ma".
3
4	definition sign_extension: Byte → Word ≝
5	λc.
6	let b ≝ get_index_v ? 8 c 1 ? in
7	[[ b; b; b; b; b; b; b; b ]] @@ c.
8	normalize;
9	repeat (@ (le_S_S ?));
10	@ (le_O_n);
11	qed.
12
13	lemma inclusive_disjunction_true:
14	∀b, c: bool.
15	(orb b c) = true → b = true ∨ c = true.
16	# b
17	# c
18	elim b
19	[ normalize
20	# H
21	@ or_introl
22	%
23	\| normalize
24	/2/
25	]
26	qed.
27
28	lemma conjunction_true:
29	∀b, c: bool.
30	andb b c = true → b = true ∧ c = true.
31	# b
32	# c
33	elim b
34	normalize
35	[ /2/
36	\| # K
37	destruct
38	]
39	qed.
40
41	lemma eq_true_false: false=true → False.
42	# K
43	destruct
44	qed.
45
46	lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
47	# a
48	# b
49	cases a
50	cases b
51	normalize
52	//
53	# K
54	cases (eq_true_false K)
55	qed.
56
57	lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
58	# b
59	cases b
60	%
61	qed.
62
63	lemma is_a_to_mem_to_is_in:
64	∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
65	# he
66	# a
67	# m
68	# q
69	elim q
70	[ normalize
71	# _
72	# K
73	assumption
74	\| # m'
75	# t
76	# q'
77	# II
78	# H1
79	# H2
80	normalize
81	change in H2: (??%?) with (orb ??)
82	cases (inclusive_disjunction_true … H2)
83	[ # K
84	< (eq_a_to_eq … K)
85	> H1
86	%
87	\| # K
88	> II
89	try assumption
90	cases (is_a t a)
91	normalize
92	%
93	]
94	]
95	qed.
96
97	lemma execute_1_technical:
98	∀n, m: nat.
99	∀v: Vector addressing_mode_tag (S n).
100	∀q: Vector addressing_mode_tag (S m).
101	∀a: addressing_mode.
102	bool_to_Prop (is_in ? v a) →
103	bool_to_Prop (subvector_with ? ? ? eq_a v q) →
104	bool_to_Prop (is_in ? q a).
105	# n
106	# m
107	# v
108	# q
109	# a
110	elim v
111	[ normalize
112	# K
113	cases K
114	\| # n'
115	# he
116	# tl
117	# II
118	whd in ⊢ (% → ? → ?)
119	lapply (refl … (is_in … (he:::tl) a))
120	cases (is_in … (he:::tl) a) in ⊢ (???% → %)
121	[ # K
122	# _
123	normalize in K;
124	whd in ⊢ (% → ?)
125	lapply (refl … (subvector_with … eq_a (he:::tl) q))
126	cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
127	[ # K1
128	# _
129	change in K1 with ((andb ? (subvector_with …)) = true)
130	cases (conjunction_true … K1)
131	# K3
132	# K4
133	cases (inclusive_disjunction_true … K)
134	# K2
135	[ > (is_a_to_mem_to_is_in … K2 K3)
136	%
137	\| @ II
138	[ > K2
139	%
140	\| > K4
141	%
142	]
143	]
144	\| # K1
145	# K2
146	(normalize in K2)
147	cases K2;
148	]
149	\| # K1
150	# K2
151	normalize in K2;
152	cases K2
153	]
154	]
155	qed.
156
157	include alias "arithmetics/nat.ma".
158	include alias "ASM/BitVectorTrie.ma".
159
160	definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
161	λA, M: Type[0].
162	λaddr_of: A → (PreStatus M) → Word.
163	λinstr: preinstruction A.
164	λs: PreStatus M.
165	match instr with
166	[ ADD addr1 addr2 ⇒
167	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
168	(get_arg_8 ? s false addr2) false in
169	let cy_flag ≝ get_index' ? O ? flags in
170	let ac_flag ≝ get_index' ? 1 ? flags in
171	let ov_flag ≝ get_index' ? 2 ? flags in
172	let s ≝ set_arg_8 ? s ACC_A result in
173	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
174	\| ADDC addr1 addr2 ⇒
175	let old_cy_flag ≝ get_cy_flag ? s in
176	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
177	(get_arg_8 ? s false addr2) old_cy_flag in
178	let cy_flag ≝ get_index' ? O ? flags in
179	let ac_flag ≝ get_index' ? 1 ? flags in
180	let ov_flag ≝ get_index' ? 2 ? flags in
181	let s ≝ set_arg_8 ? s ACC_A result in
182	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
183	\| SUBB addr1 addr2 ⇒
184	let old_cy_flag ≝ get_cy_flag ? s in
185	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
186	(get_arg_8 ? s false addr2) old_cy_flag in
187	let cy_flag ≝ get_index' ? O ? flags in
188	let ac_flag ≝ get_index' ? 1 ? flags in
189	let ov_flag ≝ get_index' ? 2 ? flags in
190	let s ≝ set_arg_8 ? s ACC_A result in
191	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
192	\| ANL addr ⇒
193	match addr with
194	[ inl l ⇒
195	match l with
196	[ inl l' ⇒
197	let 〈addr1, addr2〉 ≝ l' in
198	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
199	set_arg_8 ? s addr1 and_val
200	\| inr r ⇒
201	let 〈addr1, addr2〉 ≝ r in
202	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
203	set_arg_8 ? s addr1 and_val
204	]
205	\| inr r ⇒
206	let 〈addr1, addr2〉 ≝ r in
207	let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
208	set_flags ? s and_val (None ?) (get_ov_flag ? s)
209	]
210	\| ORL addr ⇒
211	match addr with
212	[ inl l ⇒
213	match l with
214	[ inl l' ⇒
215	let 〈addr1, addr2〉 ≝ l' in
216	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
217	set_arg_8 ? s addr1 or_val
218	\| inr r ⇒
219	let 〈addr1, addr2〉 ≝ r in
220	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
221	set_arg_8 ? s addr1 or_val
222	]
223	\| inr r ⇒
224	let 〈addr1, addr2〉 ≝ r in
225	let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
226	set_flags ? s or_val (None ?) (get_ov_flag ? s)
227	]
228	\| XRL addr ⇒
229	match addr with
230	[ inl l' ⇒
231	let 〈addr1, addr2〉 ≝ l' in
232	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
233	set_arg_8 ? s addr1 xor_val
234	\| inr r ⇒
235	let 〈addr1, addr2〉 ≝ r in
236	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
237	set_arg_8 ? s addr1 xor_val
238	]
239	\| INC addr ⇒
240	match addr return λx. bool_to_Prop (is_in … [[ acc_a;
241	registr;
242	direct;
243	indirect;
244	dptr ]] x) → ? with
245	[ ACC_A ⇒ λacc_a: True.
246	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
247	set_arg_8 ? s ACC_A result
248	\| REGISTER r ⇒ λregister: True.
249	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
250	set_arg_8 ? s (REGISTER r) result
251	\| DIRECT d ⇒ λdirect: True.
252	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
253	set_arg_8 ? s (DIRECT d) result
254	\| INDIRECT i ⇒ λindirect: True.
255	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
256	set_arg_8 ? s (INDIRECT i) result
257	\| DPTR ⇒ λdptr: True.
258	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
259	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
260	let s ≝ set_8051_sfr ? s SFR_DPL bl in
261	set_8051_sfr ? s SFR_DPH bu
262	\| _ ⇒ λother: False. ⊥
263	] (subaddressing_modein … addr)
264	\| DEC addr ⇒
265	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
266	set_arg_8 ? s addr result
267	\| MUL addr1 addr2 ⇒
268	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
269	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
270	let product ≝ acc_a_nat * acc_b_nat in
271	let ov_flag ≝ product ≥ 256 in
272	let low ≝ bitvector_of_nat 8 (product mod 256) in
273	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
274	let s ≝ set_8051_sfr ? s SFR_ACC_A low in
275	set_8051_sfr ? s SFR_ACC_B high
276	\| DIV addr1 addr2 ⇒
277	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
278	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
279	match acc_b_nat with
280	[ O ⇒ set_flags ? s false (None Bit) true
281	\| S o ⇒
282	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
283	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
284	let s ≝ set_8051_sfr ? s SFR_ACC_A q in
285	let s ≝ set_8051_sfr ? s SFR_ACC_B r in
286	set_flags ? s false (None Bit) false
287	]
288	\| DA addr ⇒
289	let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
290	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
291	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
292	let cy_flag ≝ get_index' ? O ? flags in
293	let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
294	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
295	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
296	let new_acc ≝ nu @@ acc_nl' in
297	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
298	set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
299	else
300	s
301	else
302	s
303	\| CLR addr ⇒
304	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
305	[ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
306	\| CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
307	\| BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
308	\| _ ⇒ λother: False. ⊥
309	] (subaddressing_modein … addr)
310	\| CPL addr ⇒
311	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
312	[ ACC_A ⇒ λacc_a: True.
313	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
314	let new_acc ≝ negation_bv ? old_acc in
315	set_8051_sfr ? s SFR_ACC_A new_acc
316	\| CARRY ⇒ λcarry: True.
317	let old_cy_flag ≝ get_arg_1 ? s CARRY true in
318	let new_cy_flag ≝ ¬old_cy_flag in
319	set_arg_1 ? s CARRY new_cy_flag
320	\| BIT_ADDR b ⇒ λbit_addr: True.
321	let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
322	let new_bit ≝ ¬old_bit in
323	set_arg_1 ? s (BIT_ADDR b) new_bit
324	\| _ ⇒ λother: False. ?
325	] (subaddressing_modein … addr)
326	\| SETB b ⇒ set_arg_1 ? s b false
327	\| RL _ ⇒ (* DPM: always ACC_A *)
328	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
329	let new_acc ≝ rotate_left … 1 old_acc in
330	set_8051_sfr ? s SFR_ACC_A new_acc
331	\| RR _ ⇒ (* DPM: always ACC_A *)
332	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
333	let new_acc ≝ rotate_right … 1 old_acc in
334	set_8051_sfr ? s SFR_ACC_A new_acc
335	\| RLC _ ⇒ (* DPM: always ACC_A *)
336	let old_cy_flag ≝ get_cy_flag ? s in
337	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
338	let new_cy_flag ≝ get_index' ? O ? old_acc in
339	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
340	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
341	set_8051_sfr ? s SFR_ACC_A new_acc
342	\| RRC _ ⇒ (* DPM: always ACC_A *)
343	let old_cy_flag ≝ get_cy_flag ? s in
344	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
345	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
346	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
347	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
348	set_8051_sfr ? s SFR_ACC_A new_acc
349	\| SWAP _ ⇒ (* DPM: always ACC_A *)
350	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
351	let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
352	let new_acc ≝ nl @@ nu in
353	set_8051_sfr ? s SFR_ACC_A new_acc
354	\| PUSH addr ⇒
355	match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
356	[ DIRECT d ⇒ λdirect: True.
357	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
358	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
359	write_at_stack_pointer ? s d
360	\| _ ⇒ λother: False. ⊥
361	] (subaddressing_modein … addr)
362	\| POP addr ⇒
363	let contents ≝ read_at_stack_pointer ? s in
364	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
365	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
366	set_arg_8 ? s addr contents
367	\| XCH addr1 addr2 ⇒
368	let old_addr ≝ get_arg_8 ? s false addr2 in
369	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
370	let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
371	set_arg_8 ? s addr2 old_acc
372	\| XCHD addr1 addr2 ⇒
373	let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
374	let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
375	let new_acc ≝ acc_nu @@ arg_nl in
376	let new_arg ≝ arg_nu @@ acc_nl in
377	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
378	set_arg_8 ? s addr2 new_arg
379	\| RET ⇒
380	let high_bits ≝ read_at_stack_pointer ? s in
381	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
382	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
383	let low_bits ≝ read_at_stack_pointer ? s in
384	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
385	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
386	let new_pc ≝ high_bits @@ low_bits in
387	set_program_counter ? s new_pc
388	\| RETI ⇒
389	let high_bits ≝ read_at_stack_pointer ? s in
390	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
391	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
392	let low_bits ≝ read_at_stack_pointer ? s in
393	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
394	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
395	let new_pc ≝ high_bits @@ low_bits in
396	set_program_counter ? s new_pc
397	\| MOVX addr ⇒
398	(* DPM: only copies --- doesn't affect I/O *)
399	match addr with
400	[ inl l ⇒
401	let 〈addr1, addr2〉 ≝ l in
402	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
403	\| inr r ⇒
404	let 〈addr1, addr2〉 ≝ r in
405	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
406	]
407	\| MOV addr ⇒
408	match addr with
409	[ inl l ⇒
410	match l with
411	[ inl l' ⇒
412	match l' with
413	[ inl l'' ⇒
414	match l'' with
415	[ inl l''' ⇒
416	match l''' with
417	[ inl l'''' ⇒
418	let 〈addr1, addr2〉 ≝ l'''' in
419	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
420	\| inr r'''' ⇒
421	let 〈addr1, addr2〉 ≝ r'''' in
422	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
423	]
424	\| inr r''' ⇒
425	let 〈addr1, addr2〉 ≝ r''' in
426	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
427	]
428	\| inr r'' ⇒
429	let 〈addr1, addr2〉 ≝ r'' in
430	set_arg_16 ? s (get_arg_16 ? s addr2) addr1
431	]
432	\| inr r ⇒
433	let 〈addr1, addr2〉 ≝ r in
434	set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
435	]
436	\| inr r ⇒
437	let 〈addr1, addr2〉 ≝ r in
438	set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
439	]
440	\| JC addr ⇒
441	if get_cy_flag ? s then
442	set_program_counter ? s (addr_of addr s)
443	else
444	s
445	\| JNC addr ⇒
446	if ¬(get_cy_flag ? s) then
447	set_program_counter ? s (addr_of addr s)
448	else
449	s
450	\| JB addr1 addr2 ⇒
451	if get_arg_1 ? s addr1 false then
452	set_program_counter ? s (addr_of addr2 s)
453	else
454	s
455	\| JNB addr1 addr2 ⇒
456	if ¬(get_arg_1 ? s addr1 false) then
457	set_program_counter ? s (addr_of addr2 s)
458	else
459	s
460	\| JBC addr1 addr2 ⇒
461	let s ≝ set_arg_1 ? s addr1 false in
462	if get_arg_1 ? s addr1 false then
463	set_program_counter ? s (addr_of addr2 s)
464	else
465	s
466	\| JZ addr ⇒
467	if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
468	set_program_counter ? s (addr_of addr s)
469	else
470	s
471	\| JNZ addr ⇒
472	if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
473	set_program_counter ? s (addr_of addr s)
474	else
475	s
476	\| CJNE addr1 addr2 ⇒
477	match addr1 with
478	[ inl l ⇒
479	let 〈addr1, addr2'〉 ≝ l in
480	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
481	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
482	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
483	let s ≝ set_program_counter ? s (addr_of addr2 s) in
484	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
485	else
486	(set_flags ? s new_cy (None ?) (get_ov_flag ? s))
487	\| inr r' ⇒
488	let 〈addr1, addr2'〉 ≝ r' in
489	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
490	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
491	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
492	let s ≝ set_program_counter ? s (addr_of addr2 s) in
493	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
494	else
495	(set_flags ? s new_cy (None ?) (get_ov_flag ? s))
496	]
497	\| DJNZ addr1 addr2 ⇒
498	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
499	let s ≝ set_arg_8 ? s addr1 result in
500	if ¬(eq_bv ? result (zero 8)) then
501	set_program_counter ? s (addr_of addr2 s)
502	else
503	s
504	\| NOP ⇒ s
505	].
506	try assumption
507	try (
508	normalize
509	repeat (@ (le_S_S))
510	@ (le_O_n)
511	)
512	try (
513	@ (execute_1_technical … (subaddressing_modein …))
514	@ I
515	)
516	try (
517	normalize
518	@ I
519	)
520	qed.
521
522	definition execute_1: Status → Status ≝
523	λs: Status.
524	let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in
525	let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
526	let s ≝ set_clock ? s (clock ? s + ticks) in
527	let s ≝ set_program_counter ? s pc in
528	let s ≝
529	match instr with
530	[ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
531	(λx. λs.
532	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
533	[ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
534	\| _ ⇒ λabsd. ⊥
535	] (subaddressing_modein … x)) instr s
536	\| ACALL addr ⇒
537	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
538	[ ADDR11 a ⇒ λaddr11: True.
539	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
540	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
541	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
542	let s ≝ write_at_stack_pointer ? s pc_bl in
543	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
544	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
545	let s ≝ write_at_stack_pointer ? s pc_bu in
546	let 〈thr, eig〉 ≝ split ? 3 8 a in
547	let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
548	let new_addr ≝ (fiv @@ thr) @@ pc_bl in
549	set_program_counter ? s new_addr
550	\| _ ⇒ λother: False. ⊥
551	] (subaddressing_modein … addr)
552	\| LCALL addr ⇒
553	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
554	[ ADDR16 a ⇒ λaddr16: True.
555	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
556	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
557	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
558	let s ≝ write_at_stack_pointer ? s pc_bl in
559	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
560	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
561	let s ≝ write_at_stack_pointer ? s pc_bu in
562	set_program_counter ? s a
563	\| _ ⇒ λother: False. ⊥
564	] (subaddressing_modein … addr)
565	\| MOVC addr1 addr2 ⇒
566	match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
567	[ ACC_DPTR ⇒ λacc_dptr: True.
568	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
569	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
570	let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
571	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
572	set_8051_sfr ? s SFR_ACC_A result
573	\| ACC_PC ⇒ λacc_pc: True.
574	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
575	let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
576	(* DPM: Under specified: does the carry from PC incrementation affect the *)
577	(* addition of the PC with the DPTR? At the moment, no. *)
578	let s ≝ set_program_counter ? s inc_pc in
579	let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
580	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
581	set_8051_sfr ? s SFR_ACC_A result
582	\| _ ⇒ λother: False. ⊥
583	] (subaddressing_modein … addr2)
584	\| JMP _ ⇒ (* DPM: always indirect_dptr *)
585	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
586	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
587	let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
588	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
589	set_program_counter ? s new_pc
590	\| LJMP addr ⇒
591	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
592	[ ADDR16 a ⇒ λaddr16: True.
593	set_program_counter ? s a
594	\| _ ⇒ λother: False. ⊥
595	] (subaddressing_modein … addr)
596	\| SJMP addr ⇒
597	match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
598	[ RELATIVE r ⇒ λrelative: True.
599	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
600	set_program_counter ? s new_pc
601	\| _ ⇒ λother: False. ⊥
602	] (subaddressing_modein … addr)
603	\| AJMP addr ⇒
604	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
605	[ ADDR11 a ⇒ λaddr11: True.
606	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
607	let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
608	let bit ≝ get_index' ? O ? nl in
609	let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
610	let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
611	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
612	set_program_counter ? s new_pc
613	\| _ ⇒ λother: False. ⊥
614	] (subaddressing_modein … addr)
615	]
616	in
617	s.
618	try assumption
619	try (
620	normalize
621	repeat (@ (le_S_S))
622	@ (le_O_n)
623	)
624	try (
625	@ (execute_1_technical … (subaddressing_modein …))
626	@ I
627	)
628	try (
629	normalize
630	@ I
631	)
632	qed.
633
634	let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
635	match l with
636	[ nil ⇒ ?
637	\| cons hd tl ⇒
638	if pred hd then
639	acc
640	else
641	index_of_internal A pred tl (S acc)
642	].
643	cases not_implemented.
644	qed.
645
646	definition index_of ≝
647	λA.
648	λeq.
649	λl.
650	index_of_internal A eq l 0.
651
652	definition address_of_word_labels_internal ≝
653	λy: Identifier.
654	λx: labelled_instruction.
655	match \fst x with
656	[ None ⇒ false
657	\| Some x ⇒ eq_bv ? x y
658	].
659
660	definition address_of_word_labels_code_mem ≝
661	λcode_mem.
662	λid: Identifier.
663	bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem).
664
665	definition address_of_word_labels ≝
666	λps: PseudoStatus.
667	λid: Identifier.
668	address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
669
670	definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
671	λticks_of.
672	λs.
673	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
674	let ticks ≝ ticks_of (program_counter ? s) in
675	let s ≝ set_clock ? s (clock ? s + ticks) in
676	let s ≝ set_program_counter ? s pc in
677	let s ≝
678	match instr with
679	[ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
680	\| Comment cmt ⇒ s
681	\| Cost cst ⇒ s
682	\| Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
683	\| Call call ⇒
684	let a ≝ address_of_word_labels s call in
685	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
686	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
687	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
688	let s ≝ write_at_stack_pointer ? s pc_bl in
689	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
690	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
691	let s ≝ write_at_stack_pointer ? s pc_bu in
692	set_program_counter ? s a
693	\| Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
694	]
695	in
696	s.
697	normalize
698	@ I
699	qed.
700
701	let rec execute (n: nat) (s: Status) on n: Status ≝
702	match n with
703	[ O ⇒ s
704	\| S o ⇒ execute o (execute_1 s)
705	].
706
707	let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝
708	match n with
709	[ O ⇒ s
710	\| S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
711	].

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

Download in other formats:

Original Format