Context Navigation

Interpret.ma @ 1582

Last change on this file since 1582 was 1582, checked in by mulligan, 9 years ago
more added to the proof of execute_1_preinstruction --- ~260 cases now reduced to less than 20
File size: 39.2 KB

Line
1	include "ASM/Status.ma".
2	include "ASM/Fetch.ma".
3	include "ASM/JMCoercions.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	//
21	# K
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
123	lemma set_flags_ignores_clock:
124	∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
125	//
126	qed.
127
128	lemma set_arg_8_ignores_clock:
129	∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
130	#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
131	#a #E >E //
132	qed.
133
134	lemma set_program_counter_ignores_clock:
135	∀M: Type[0].
136	∀s: PreStatus M.
137	∀pc: Word.
138	clock M (set_program_counter … s pc) = clock … s.
139	#M #s #pc %
140	qed.
141
142	lemma set_low_internal_ram_ignores_clock:
143	∀M: Type[0].
144	∀s: PreStatus M.
145	∀ram: BitVectorTrie Byte 7.
146	clock … (set_low_internal_ram … s ram) = clock … s.
147	#M #s #ram %
148	qed.
149
150	lemma set_high_internal_ram_ignores_clock:
151	∀m: Type[0].
152	∀s: PreStatus m.
153	∀ram: BitVectorTrie Byte 7.
154	clock … (set_high_internal_ram … s ram) = clock … s.
155	#m #s #ram %
156	qed.
157
158	lemma set_8051_sfr_ignores_clock:
159	∀M: Type[0].
160	∀s: PreStatus M.
161	∀sfr: SFR8051.
162	∀v: Byte.
163	clock … (set_8051_sfr ? s sfr v) = clock … s.
164	#M #s #sfr #v %
165	qed.
166
167	lemma set_arg_1_ignores_clock:
168	∀m: Type[0].
169	∀s: PreStatus m.
170	∀addr: [[bit_addr; carry]].
171	∀bit: Bit.
172	clock … (set_arg_1 m s addr bit) = clock … s.
173	#m #s #addr #bit
174	whd in match set_arg_1; normalize nodelta
175	cases addr #subaddressing_mode
176	cases subaddressing_mode
177	try #assm1 try #assm2
178	try (normalize in assm2; cases assm2)
179	try (normalize in assm1; cases assm1)
180	normalize nodelta
181	cases (split bool 4 4 (get_8051_sfr m s SFR_PSW))
182	#nu #nl normalize nodelta
183	[ @set_8051_sfr_ignores_clock
184	\| cases(split … 1 3 nu)
185	#ignore #three_bits normalize nodelta
186	cases(get_index_v … 4 nu 0 ?)
187	normalize nodelta
188	[ <set_bit_addressable_sfr_ignores_clock \| >set_low_internal_ram_ignores_clock ] %
189	]
190	qed.
191
192	lemma set_arg_16_ignores_clock:
193	∀m: Type[0].
194	∀s: PreStatus m.
195	∀w: Word.
196	∀addr: [[dptr]].
197	clock … (set_arg_16 m s w addr) = clock … s.
198	#m #s #w #addr
199	whd in match set_arg_16; normalize nodelta
200	cases addr #subaddressing_modein
201	cases subaddressing_modein
202	try #assm1 try #assm2
203	try (normalize in assm2; cases assm2)
204	try (normalize in assm1; cases assm1)
205	normalize nodelta
206	cases (split … 8 8 w) #bu #bl normalize nodelta
207	>set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock %
208	qed.
209
210	lemma write_at_stack_pointer_ignores_clock:
211	∀m: Type[0].
212	∀s: PreStatus m.
213	∀v: Byte.
214	clock … (write_at_stack_pointer m s v) = clock … s.
215	#m #s #v
216	whd in match write_at_stack_pointer; normalize nodelta
217	cases(split … 4 4 ?) #nu #nl normalize nodelta
218	cases(get_index_v … 4 nu 0 ?) normalize nodelta
219	[ >set_low_internal_ram_ignores_clock \| >set_high_internal_ram_ignores_clock ] %
220	qed.
221
222	lemma clock_set_clock:
223	∀M: Type[0].
224	∀s: PreStatus M.
225	∀v.
226	clock … (set_clock … s v) = v.
227	#M #s #v %
228	qed.
229
230	definition execute_1_preinstruction:
231	∀ticks: nat × nat.
232	∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
233	∀s: PreStatus m.
234	Σs': PreStatus m.
235	Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝
236	λticks: nat × nat.
237	λa, m: Type[0].
238	λaddr_of: a → PreStatus m → Word.
239	λinstr: preinstruction a.
240	λs: PreStatus m.
241	let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in
242	let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in
243	match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
244	[ ADD addr1 addr2 ⇒
245	let s ≝ add_ticks1 s in
246	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
247	(get_arg_8 ? s false addr2) false in
248	let cy_flag ≝ get_index' ? O ? flags in
249	let ac_flag ≝ get_index' ? 1 ? flags in
250	let ov_flag ≝ get_index' ? 2 ? flags in
251	let s ≝ set_arg_8 ? s ACC_A result in
252	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
253	\| ADDC addr1 addr2 ⇒
254	let s ≝ add_ticks1 s in
255	let old_cy_flag ≝ get_cy_flag ? s in
256	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
257	(get_arg_8 ? s false addr2) old_cy_flag in
258	let cy_flag ≝ get_index' ? O ? flags in
259	let ac_flag ≝ get_index' ? 1 ? flags in
260	let ov_flag ≝ get_index' ? 2 ? flags in
261	let s ≝ set_arg_8 ? s ACC_A result in
262	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
263	\| SUBB addr1 addr2 ⇒
264	let s ≝ add_ticks1 s in
265	let old_cy_flag ≝ get_cy_flag ? s in
266	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
267	(get_arg_8 ? s false addr2) old_cy_flag in
268	let cy_flag ≝ get_index' ? O ? flags in
269	let ac_flag ≝ get_index' ? 1 ? flags in
270	let ov_flag ≝ get_index' ? 2 ? flags in
271	let s ≝ set_arg_8 ? s ACC_A result in
272	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
273	\| ANL addr ⇒
274	let s ≝ add_ticks1 s in
275	match addr with
276	[ inl l ⇒
277	match l with
278	[ inl l' ⇒
279	let 〈addr1, addr2〉 ≝ l' in
280	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
281	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
282	\| inr r ⇒
283	let 〈addr1, addr2〉 ≝ r in
284	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
285	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
286	]
287	\| inr r ⇒
288	let 〈addr1, addr2〉 ≝ r in
289	let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
290	eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s))
291	]
292	\| ORL addr ⇒
293	let s ≝ add_ticks1 s in
294	match addr with
295	[ inl l ⇒
296	match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
297	[ inl l' ⇒
298	let 〈addr1, addr2〉 ≝ l' in
299	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
300	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
301	\| inr r ⇒
302	let 〈addr1, addr2〉 ≝ r in
303	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
304	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
305	]
306	\| inr r ⇒
307	let 〈addr1, addr2〉 ≝ r in
308	let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
309	eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s))
310	]
311	\| XRL addr ⇒
312	let s ≝ add_ticks1 s in
313	match addr with
314	[ inl l' ⇒
315	let 〈addr1, addr2〉 ≝ l' in
316	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
317	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
318	\| inr r ⇒
319	let 〈addr1, addr2〉 ≝ r in
320	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
321	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
322	]
323	\| INC addr ⇒
324	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
325	[ ACC_A ⇒ λacc_a: True.
326	let s' ≝ add_ticks1 s in
327	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
328	eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result)
329	\| REGISTER r ⇒ λregister: True.
330	let s' ≝ add_ticks1 s in
331	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
332	eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result)
333	\| DIRECT d ⇒ λdirect: True.
334	let s' ≝ add_ticks1 s in
335	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
336	eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result)
337	\| INDIRECT i ⇒ λindirect: True.
338	let s' ≝ add_ticks1 s in
339	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
340	eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result)
341	\| DPTR ⇒ λdptr: True.
342	let s' ≝ add_ticks1 s in
343	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
344	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
345	let s ≝ set_8051_sfr ? s' SFR_DPL bl in
346	eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu)
347	\| _ ⇒ λother: False. ⊥
348	] (subaddressing_modein … addr)
349	\| NOP ⇒
350	let s ≝ add_ticks2 s in
351	s
352	\| DEC addr ⇒
353	let s ≝ add_ticks1 s in
354	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
355	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result)
356	\| MUL addr1 addr2 ⇒
357	let s ≝ add_ticks1 s in
358	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
359	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
360	let product ≝ acc_a_nat * acc_b_nat in
361	let ov_flag ≝ product ≥ 256 in
362	let low ≝ bitvector_of_nat 8 (product mod 256) in
363	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
364	let s ≝ set_8051_sfr ? s SFR_ACC_A low in
365	set_8051_sfr ? s SFR_ACC_B high
366	\| DIV addr1 addr2 ⇒
367	let s ≝ add_ticks1 s in
368	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
369	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
370	match acc_b_nat with
371	[ O ⇒ set_flags ? s false (None Bit) true
372	\| S o ⇒
373	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
374	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
375	let s ≝ set_8051_sfr ? s SFR_ACC_A q in
376	let s ≝ set_8051_sfr ? s SFR_ACC_B r in
377	set_flags ? s false (None Bit) false
378	]
379	\| DA addr ⇒
380	let s ≝ add_ticks1 s in
381	let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
382	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
383	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
384	let cy_flag ≝ get_index' ? O ? flags in
385	let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
386	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
387	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
388	let new_acc ≝ nu @@ acc_nl' in
389	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
390	set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
391	else
392	s
393	else
394	s
395	\| CLR addr ⇒
396	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
397	[ ACC_A ⇒ λacc_a: True.
398	let s ≝ add_ticks1 s in
399	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8))
400	\| CARRY ⇒ λcarry: True.
401	let s ≝ add_ticks1 s in
402	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false)
403	\| BIT_ADDR b ⇒ λbit_addr: True.
404	let s ≝ add_ticks1 s in
405	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false)
406	\| _ ⇒ λother: False. ⊥
407	] (subaddressing_modein … addr)
408	\| CPL addr ⇒
409	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
410	[ ACC_A ⇒ λacc_a: True.
411	let s ≝ add_ticks1 s in
412	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
413	let new_acc ≝ negation_bv ? old_acc in
414	eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc)
415	\| CARRY ⇒ λcarry: True.
416	let s ≝ add_ticks1 s in
417	let old_cy_flag ≝ get_arg_1 ? s CARRY true in
418	let new_cy_flag ≝ ¬old_cy_flag in
419	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag)
420	\| BIT_ADDR b ⇒ λbit_addr: True.
421	let s ≝ add_ticks1 s in
422	let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
423	let new_bit ≝ ¬old_bit in
424	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit)
425	\| _ ⇒ λother: False. ?
426	] (subaddressing_modein … addr)
427	\| SETB b ⇒
428	let s ≝ add_ticks1 s in
429	set_arg_1 ? s b false
430	\| RL _ ⇒ (* DPM: always ACC_A *)
431	let s ≝ add_ticks1 s in
432	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
433	let new_acc ≝ rotate_left … 1 old_acc in
434	set_8051_sfr ? s SFR_ACC_A new_acc
435	\| RR _ ⇒ (* DPM: always ACC_A *)
436	let s ≝ add_ticks1 s in
437	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
438	let new_acc ≝ rotate_right … 1 old_acc in
439	set_8051_sfr ? s SFR_ACC_A new_acc
440	\| RLC _ ⇒ (* DPM: always ACC_A *)
441	let s ≝ add_ticks1 s in
442	let old_cy_flag ≝ get_cy_flag ? s in
443	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
444	let new_cy_flag ≝ get_index' ? O ? old_acc in
445	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
446	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
447	set_8051_sfr ? s SFR_ACC_A new_acc
448	\| RRC _ ⇒ (* DPM: always ACC_A *)
449	let s ≝ add_ticks1 s in
450	let old_cy_flag ≝ get_cy_flag ? s in
451	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
452	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
453	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
454	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
455	set_8051_sfr ? s SFR_ACC_A new_acc
456	\| SWAP _ ⇒ (* DPM: always ACC_A *)
457	let s ≝ add_ticks1 s in
458	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
459	let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
460	let new_acc ≝ nl @@ nu in
461	set_8051_sfr ? s SFR_ACC_A new_acc
462	\| PUSH addr ⇒
463	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
464	[ DIRECT d ⇒ λdirect: True.
465	let s ≝ add_ticks1 s in
466	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
467	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
468	write_at_stack_pointer ? s d
469	\| _ ⇒ λother: False. ⊥
470	] (subaddressing_modein … addr)
471	\| POP addr ⇒
472	let s ≝ add_ticks1 s in
473	let contents ≝ read_at_stack_pointer ? s in
474	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
475	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
476	set_arg_8 ? s addr contents
477	\| XCH addr1 addr2 ⇒
478	let s ≝ add_ticks1 s in
479	let old_addr ≝ get_arg_8 ? s false addr2 in
480	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
481	let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
482	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc)
483	\| XCHD addr1 addr2 ⇒
484	let s ≝ add_ticks1 s in
485	let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
486	let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
487	let new_acc ≝ acc_nu @@ arg_nl in
488	let new_arg ≝ arg_nu @@ acc_nl in
489	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
490	set_arg_8 ? s addr2 new_arg
491	\| RET ⇒
492	let s ≝ add_ticks1 s in
493	let high_bits ≝ read_at_stack_pointer ? s in
494	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
495	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
496	let low_bits ≝ read_at_stack_pointer ? s in
497	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
498	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
499	let new_pc ≝ high_bits @@ low_bits in
500	set_program_counter ? s new_pc
501	\| RETI ⇒
502	let s ≝ add_ticks1 s in
503	let high_bits ≝ read_at_stack_pointer ? s in
504	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
505	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
506	let low_bits ≝ read_at_stack_pointer ? s in
507	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
508	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
509	let new_pc ≝ high_bits @@ low_bits in
510	set_program_counter ? s new_pc
511	\| MOVX addr ⇒
512	let s ≝ add_ticks1 s in
513	(* DPM: only copies --- doesn't affect I/O *)
514	match addr with
515	[ inl l ⇒
516	let 〈addr1, addr2〉 ≝ l in
517	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
518	\| inr r ⇒
519	let 〈addr1, addr2〉 ≝ r in
520	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
521	]
522	\| MOV addr ⇒
523	let s ≝ add_ticks1 s in
524	match addr with
525	[ inl l ⇒
526	match l with
527	[ inl l' ⇒
528	match l' with
529	[ inl l'' ⇒
530	match l'' with
531	[ inl l''' ⇒
532	match l''' with
533	[ inl l'''' ⇒
534	let 〈addr1, addr2〉 ≝ l'''' in
535	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
536	\| inr r'''' ⇒
537	let 〈addr1, addr2〉 ≝ r'''' in
538	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
539	]
540	\| inr r''' ⇒
541	let 〈addr1, addr2〉 ≝ r''' in
542	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
543	]
544	\| inr r'' ⇒
545	let 〈addr1, addr2〉 ≝ r'' in
546	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
547	]
548	\| inr r ⇒
549	let 〈addr1, addr2〉 ≝ r in
550	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
551	]
552	\| inr r ⇒
553	let 〈addr1, addr2〉 ≝ r in
554	eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
555	]
556	\| JC addr ⇒
557	if get_cy_flag ? s then
558	let s ≝ add_ticks1 s in
559	set_program_counter ? s (addr_of addr s)
560	else
561	let s ≝ add_ticks2 s in
562	s
563	\| JNC addr ⇒
564	if ¬(get_cy_flag ? s) then
565	let s ≝ add_ticks1 s in
566	set_program_counter ? s (addr_of addr s)
567	else
568	let s ≝ add_ticks2 s in
569	s
570	\| JB addr1 addr2 ⇒
571	if get_arg_1 ? s addr1 false then
572	let s ≝ add_ticks1 s in
573	set_program_counter ? s (addr_of addr2 s)
574	else
575	let s ≝ add_ticks2 s in
576	s
577	\| JNB addr1 addr2 ⇒
578	if ¬(get_arg_1 ? s addr1 false) then
579	let s ≝ add_ticks1 s in
580	set_program_counter ? s (addr_of addr2 s)
581	else
582	let s ≝ add_ticks2 s in
583	s
584	\| JBC addr1 addr2 ⇒
585	let s ≝ set_arg_1 ? s addr1 false in
586	if get_arg_1 ? s addr1 false then
587	let s ≝ add_ticks1 s in
588	set_program_counter ? s (addr_of addr2 s)
589	else
590	let s ≝ add_ticks2 s in
591	s
592	\| JZ addr ⇒
593	if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
594	let s ≝ add_ticks1 s in
595	set_program_counter ? s (addr_of addr s)
596	else
597	let s ≝ add_ticks2 s in
598	s
599	\| JNZ addr ⇒
600	if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
601	let s ≝ add_ticks1 s in
602	set_program_counter ? s (addr_of addr s)
603	else
604	let s ≝ add_ticks2 s in
605	s
606	\| CJNE addr1 addr2 ⇒
607	match addr1 with
608	[ inl l ⇒
609	let 〈addr1, addr2'〉 ≝ l in
610	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
611	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
612	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
613	let s ≝ add_ticks1 s in
614	let s ≝ set_program_counter ? s (addr_of addr2 s) in
615	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
616	else
617	let s ≝ add_ticks2 s in
618	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
619	\| inr r' ⇒
620	let 〈addr1, addr2'〉 ≝ r' in
621	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
622	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
623	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
624	let s ≝ add_ticks1 s in
625	let s ≝ set_program_counter ? s (addr_of addr2 s) in
626	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
627	else
628	let s ≝ add_ticks2 s in
629	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
630	]
631	\| DJNZ addr1 addr2 ⇒
632	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
633	let s ≝ set_arg_8 ? s addr1 result in
634	if ¬(eq_bv ? result (zero 8)) then
635	let s ≝ add_ticks1 s in
636	set_program_counter ? s (addr_of addr2 s)
637	else
638	let s ≝ add_ticks2 s in
639	s
640	]. (15s)
641	try (cases(other))
642	try assumption (20s)
643	try % (6s)
644	try (
645	@ (execute_1_technical … (subaddressing_modein …))
646	@ I
647	) (66s)
648	try (<set_arg_8_ignores_clock normalize nodelta /demod/ %)
649	try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %)
650	try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
651	try (normalize nodelta <set_flags_ignores_clock /demod/ %)
652	try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
653	try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
654	try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus)
655	try (/demod/ normalize nodelta >clock_set_clock <set_arg_8_ignores_clock @commutative_plus)
656	try (/demod/ normalize nodelta >set_arg_1_ignores_clock >clock_set_clock @commutative_plus)
657	try (normalize nodelta >clock_set_clock >set_arg_1_ignores_clock >clock_set_clock %)
658	try (normalize nodelta <set_arg_8_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
659	try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
660	try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
661	try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %)
662	cases daemon
663	qed.
664
665	lemma write_at_stack_pointer_ignores_clock:
666	∀M.∀s: PreStatus M.
667	∀sp: Byte.
668	clock … (write_at_stack_pointer … s sp) = clock … s.
669	#M #s #sp
670	change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
671	in match (write_at_stack_pointer ???);
672	normalize nodelta
673	cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
674	#nu #nl normalize nodelta;
675	cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
676	normalize nodelta; %
677	qed.
678
679	definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
680	Σs': Status. clock … s' = \snd current + clock … s ≝
681	λs0,instr_pc_ticks.
682	let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
683	let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
684	let s ≝ set_program_counter ? s0 pc in
685	match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0 with
686	[ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
687	(λx. λs.
688	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
689	[ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
690	\| _ ⇒ λabsd. ⊥
691	] (subaddressing_modein … x)) instr s)
692	\| MOVC addr1 addr2 ⇒
693	let s ≝ set_clock ? s (ticks + clock ? s) in
694	match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
695	[ ACC_DPTR ⇒ λacc_dptr: True.
696	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
697	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
698	let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
699	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
700	set_8051_sfr ? s SFR_ACC_A result
701	\| ACC_PC ⇒ λacc_pc: True.
702	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
703	let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
704	(* DPM: Under specified: does the carry from PC incrementation affect the *)
705	(* addition of the PC with the DPTR? At the moment, no. *)
706	let s ≝ set_program_counter ? s inc_pc in
707	let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
708	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
709	set_8051_sfr ? s SFR_ACC_A result
710	\| _ ⇒ λother: False. ⊥
711	] (subaddressing_modein … addr2)
712	\| JMP _ ⇒ (* DPM: always indirect_dptr *)
713	let s ≝ set_clock ? s (ticks + clock ? s) in
714	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
715	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
716	let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
717	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
718	set_program_counter ? s new_pc
719	\| LJMP addr ⇒
720	let s ≝ set_clock ? s (ticks + clock ? s) in
721	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
722	[ ADDR16 a ⇒ λaddr16: True.
723	set_program_counter ? s a
724	\| _ ⇒ λother: False. ⊥
725	] (subaddressing_modein … addr)
726	\| SJMP addr ⇒
727	let s ≝ set_clock ? s (ticks + clock ? s) in
728	match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
729	[ RELATIVE r ⇒ λrelative: True.
730	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
731	set_program_counter ? s new_pc
732	\| _ ⇒ λother: False. ⊥
733	] (subaddressing_modein … addr)
734	\| AJMP addr ⇒
735	let s ≝ set_clock ? s (ticks + clock ? s) in
736	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
737	[ ADDR11 a ⇒ λaddr11: True.
738	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
739	let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
740	let bit ≝ get_index' ? O ? nl in
741	let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
742	let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
743	let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
744	set_program_counter ? s new_pc
745	\| _ ⇒ λother: False. ⊥
746	] (subaddressing_modein … addr)
747	\| ACALL addr ⇒
748	let s ≝ set_clock ? s (ticks + clock ? s) in
749	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
750	[ ADDR11 a ⇒ λaddr11: True.
751	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
752	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
753	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
754	let s ≝ write_at_stack_pointer ? s pc_bl in
755	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
756	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
757	let s ≝ write_at_stack_pointer ? s pc_bu in
758	let 〈thr, eig〉 ≝ split ? 3 8 a in
759	let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
760	let new_addr ≝ (fiv @@ thr) @@ pc_bl in
761	set_program_counter ? s new_addr
762	\| _ ⇒ λother: False. ⊥
763	] (subaddressing_modein … addr)
764	\| LCALL addr ⇒
765	let s ≝ set_clock ? s (ticks + clock ? s) in
766	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
767	[ ADDR16 a ⇒ λaddr16: True.
768	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
769	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
770	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
771	let s ≝ write_at_stack_pointer ? s pc_bl in
772	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
773	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
774	let s ≝ write_at_stack_pointer ? s pc_bu in
775	set_program_counter ? s a
776	\| _ ⇒ λother: False. ⊥
777	] (subaddressing_modein … addr)
778	]. (10s)
779	try (cases(other))
780	[2: normalize nodelta
781	>set_program_counter_ignores_clock
782	>write_at_stack_pointer_ignores_clock
783	>set_8051_sfr_ignores_clock
784	>write_at_stack_pointer_ignores_clock
785	>set_8051_sfr_ignores_clock >clock_set_clock
786	>set_program_counter_ignores_clock %
787	\|*: cases daemon
788	]
789	(*
790	[\|\|\|\|\|\|\|\|*:try assumption]
791	[1,2,3,4,5,7: @sig2 (7s)
792	\|8: cases (execute_1_preinstruction ??????) #a * #H @H]
793	[2,3: >set_program_counter_ignores_clock normalize nodelta
794	>write_at_stack_pointer_ignores_clock
795	>set_8051_sfr_ignores_clock
796	>write_at_stack_pointer_ignores_clock
797	>set_8051_sfr_ignores_clock >clock_set_clock
798	>set_program_counter_ignores_clock
799	cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ \|: #H @H] (Andrea: ???*)
800	\|1,4,5,6: >set_program_counter_ignores_clock normalize nodelta
801	>clock_set_clock >set_program_counter_ignores_clock
802	cut (∀n,m. n+m-m = n) [1,3,5,7:#n #m /by/ \|: #H @H] (Andrea: ???*)
803	\|7: >set_8051_sfr_ignores_clock normalize nodelta
804	>clock_set_clock >set_program_counter_ignores_clock
805	cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ \|*: #H @H]
806	\|8: >set_8051_sfr_ignores_clock normalize nodelta
807	>set_program_counter_ignores_clock >clock_set_clock
808	>set_program_counter_ignores_clock
809	cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ \|: #H @H]] )
810	qed.
811
812	definition current_instruction_cost ≝
813	λs: Status.
814	\snd (fetch (code_memory … s) (program_counter … s)).
815
816	definition execute_1: ∀s:Status.
817	Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝
818	λs: Status.
819	let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
820	execute_1_0 s instr_pc_ticks.
821
822	definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
823	λticks,s,instr,pc.
824	let s ≝ set_program_counter ? s pc in
825	let s ≝
826	match instr with
827	[ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
828	\| Comment cmt ⇒
829	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
830	s
831	\| Cost cst ⇒ s
832	\| Jmp jmp ⇒
833	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
834	set_program_counter ? s (address_of_word_labels s jmp)
835	\| Call call ⇒
836	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
837	let a ≝ address_of_word_labels s call in
838	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
839	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
840	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
841	let s ≝ write_at_stack_pointer ? s pc_bl in
842	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
843	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
844	let s ≝ write_at_stack_pointer ? s pc_bu in
845	set_program_counter ? s a
846	\| Mov dptr ident ⇒
847	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
848	let the_preamble ≝ \fst (code_memory ? s) in
849	let data_labels ≝ construct_datalabels the_preamble in
850	set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
851	]
852	in
853	s.
854	normalize
855	@I
856	qed.
857
858	definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
859	λticks_of,s.
860	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
861	let ticks ≝ ticks_of (program_counter ? s) in
862	execute_1_pseudo_instruction0 ticks s instr pc.
863
864	let rec execute (n: nat) (s: Status) on n: Status ≝
865	match n with
866	[ O ⇒ s
867	\| S o ⇒ execute o (execute_1 s)
868	].
869
870	let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
871	match n with
872	[ O ⇒ s
873	\| S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
874	].

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

Download in other formats:

Original Format