Context Navigation

Interpret.ma @ 1538

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

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

Download in other formats:

Original Format