Context Navigation

Interpret.ma @ 1600

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

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

Download in other formats:

Original Format