Context Navigation

AssemblyProofSplit.ma @ 1967

Last change on this file since 1967 was 1967, checked in by sacerdot, 9 years ago
Mov case completed.
File size: 25.0 KB

Line
1	include "ASM/AssemblyProof.ma".
2	include alias "arithmetics/nat.ma".
3	include alias "basics/logic.ma".
4
5	lemma set_arg_16_mk_Status_commutation:
6	∀M: Type[0].
7	∀cm: M.
8	∀s: PreStatus M cm.
9	∀w: Word.
10	∀d: [[dptr]].
11	set_arg_16 M cm s w d =
12	mk_PreStatus M cm
13	(low_internal_ram … s)
14	(high_internal_ram … s)
15	(external_ram … s)
16	(program_counter … s)
17	(special_function_registers_8051 … (set_arg_16 M cm s w d))
18	(special_function_registers_8052 … s)
19	(p1_latch … s)
20	(p3_latch … s)
21	(clock … s).
22	#M #cm #s #w #d
23	whd in match set_arg_16; normalize nodelta
24	whd in match set_arg_16'; normalize nodelta
25	@(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
26	cases (split bool 8 8 w) #bu #bl normalize nodelta
27	whd in match set_8051_sfr; normalize nodelta %
28	qed.
29
30	lemma set_program_counter_mk_Status_commutation:
31	∀M: Type[0].
32	∀cm: M.
33	∀s: PreStatus M cm.
34	∀w: Word.
35	set_program_counter M cm s w =
36	mk_PreStatus M cm
37	(low_internal_ram … s)
38	(high_internal_ram … s)
39	(external_ram … s)
40	w
41	(special_function_registers_8051 … s)
42	(special_function_registers_8052 … s)
43	(p1_latch … s)
44	(p3_latch … s)
45	(clock … s).
46	//
47	qed.
48
49	lemma set_clock_mk_Status_commutation:
50	∀M: Type[0].
51	∀cm: M.
52	∀s: PreStatus M cm.
53	∀c: nat.
54	set_clock M cm s c =
55	mk_PreStatus M cm
56	(low_internal_ram … s)
57	(high_internal_ram … s)
58	(external_ram … s)
59	(program_counter … s)
60	(special_function_registers_8051 … s)
61	(special_function_registers_8052 … s)
62	(p1_latch … s)
63	(p3_latch … s)
64	c.
65	//
66	qed.
67
68
69	lemma special_function_registers_8051_set_arg_16:
70	∀M, M': Type[0].
71	∀cm: M.
72	∀cm': M'.
73	∀s: PreStatus M cm.
74	∀s': PreStatus M' cm'.
75	∀w, w': Word.
76	∀d, d': [[dptr]].
77	special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
78	w = w' →
79	special_function_registers_8051 ?? (set_arg_16 … s w d) =
80	special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
81	#M #M' #cm #cm' #s #s' #w #w'
82	@list_addressing_mode_tags_elim_prop try %
83	@list_addressing_mode_tags_elim_prop try %
84	#EQ1 #EQ2 <EQ2 normalize cases (split bool 8 8 w) #b1 #b2 normalize <EQ1 %
85	qed.
86
87
88	theorem main_thm:
89	∀M.
90	∀M'.
91	∀program: pseudo_assembly_program.
92	∀sigma: Word → Word.
93	∀policy: Word → bool.
94	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
95	∀ps: PseudoStatus program.
96	next_internal_pseudo_address_map M program ps = Some … M' →
97	∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
98	status_of_pseudo_status M' …
99	(execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
100	#M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
101	change with (next_internal_pseudo_address_map0 ????? = ? → ?)
102	@(pose … (program_counter ?? ps)) #ppc #EQppc
103	generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
104	@pair_elim #labels #costs #create_label_cost_refl normalize nodelta
105	@pair_elim #assembled #costs' #assembly_refl normalize nodelta
106	lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
107	@pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
108	@(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
109	@(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
110	whd in match execute_1_pseudo_instruction; normalize nodelta
111	whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
112	lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
113	lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
114	[1: >fetch_pseudo_refl % ]
115	#assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
116	generalize in match assm1; -assm1 -assm2 -assm3
117	normalize nodelta
118	cases pi
119	[2,3:
120	#arg
121	(* XXX: we first work on sigma_increment_commutation *)
122	#sigma_increment_commutation
123	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
124	(* XXX: we work on the maps *)
125	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
126	(* XXX: we assume the fetch_many hypothesis *)
127	#fetch_many_assm
128	(* XXX: we give the existential *)
129	%{0}
130	whd in match (execute_1_pseudo_instruction0 ?????);
131	(* XXX: work on the left hand side of the equality *)
132	whd in ⊢ (??%?);
133	@split_eq_status //
134	[1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (CSC: auto not working, why? ) ]
135	\|6: (* Mov *)
136	#arg1 #arg2
137	(* XXX: we first work on sigma_increment_commutation *)
138	#sigma_increment_commutation
139	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
140	(* XXX: we work on the maps *)
141	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
142	(* XXX: we assume the fetch_many hypothesis *)
143	#fetch_many_assm
144	(* XXX: we give the existential *)
145	%{1}
146	whd in match (execute_1_pseudo_instruction0 ?????);
147	(* XXX: work on the left hand side of the equality *)
148	whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
149	(* XXX: execute fetches some more *)
150	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
151	whd in fetch_many_assm;
152	>EQassembled in fetch_many_assm;
153	cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
154	#eq_instr #EQticks whd in EQticks:(???%); >EQticks
155	#fetch_many_assm whd in fetch_many_assm;
156	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
157	>(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
158	(* XXX: now we start to work on the mk_PreStatus equality *)
159	change with (set_arg_16 ????? = ?)
160	>set_program_counter_mk_Status_commutation
161	>set_clock_mk_Status_commutation
162	>set_arg_16_mk_Status_commutation
163
164	change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
165	>set_program_counter_mk_Status_commutation
166	>set_clock_mk_Status_commutation
167	>set_arg_16_mk_Status_commutation in ⊢ (???%);
168
169
170	@split_eq_status //
171	[1:
172	assumption
173	\|2:
174	@special_function_registers_8051_set_arg_16
175	[2: >EQlookup_datalabels %
176	\|1: //
177	]
178	]
179
180	\|4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
181	@Some_Some_elim #MAP cases (pol ?) normalize nodelta
182	[3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
183	whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
184	@pair_elim' * #instr #newppc' #ticks #EQ4
185	* * #H2a #H2b whd in ⊢ (% → ?) #H2
186	>H2b >(eq_instruction_to_eq … H2a)
187	#EQ %[@1]
188	<MAP >(eq_bv_eq … H2) >EQ
189	whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
190	cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
191	whd in ⊢ (??%?)
192	whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
193	cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
194	\|6: (* Mov *) #arg1 #arg2
195	#H1 #H2 #EQ %[@1]
196	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
197	change in ⊢ (? → ??%?) with (execute_1_0 ??)
198	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
199	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
200	>H2b >(eq_instruction_to_eq … H2a)
201	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
202	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
203	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
204	normalize nodelta;
205	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
206	#result #flags
207	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
208	\|5: (* Call *) #label #MAP
209	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
210	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
211	[ (* short *) #abs @⊥ destruct (abs)
212	\|3: (* long *) #H1 #H2 #EQ %[@1]
213	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
214	change in ⊢ (? → ??%?) with (execute_1_0 ??)
215	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
216	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
217	>H2b >(eq_instruction_to_eq … H2a)
218	generalize in match EQ; -EQ;
219	whd in ⊢ (???% → ??%?);
220	generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
221	>(eq_bv_eq … H2c)
222	change with
223	((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
224	(let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
225	generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
226	generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
227	>get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
228	>get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
229	generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
230	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
231	@split_eq_status;
232	[ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
233	>code_memory_write_at_stack_pointer %
234	\| >set_program_counter_set_low_internal_ram
235	>set_clock_set_low_internal_ram
236	@low_internal_ram_write_at_stack_pointer
237	[ >EQ0 @pol \| % \| %
238	\| @( … EQ1)
239	\| @(pair_destruct_2 … EQ2)
240	\| >(pair_destruct_1 ????? EQpc)
241	>(pair_destruct_2 ????? EQpc)
242	@split_elim #x #y #H <H -x y H;
243	>(pair_destruct_1 ????? EQppc)
244	>(pair_destruct_2 ????? EQppc)
245	@split_elim #x #y #H <H -x y H;
246	>EQ0 % ]
247	\| >set_low_internal_ram_set_high_internal_ram
248	>set_program_counter_set_high_internal_ram
249	>set_clock_set_high_internal_ram
250	@high_internal_ram_write_at_stack_pointer
251	[ >EQ0 @pol \| % \| %
252	\| @(pair_destruct_2 … EQ1)
253	\| @(pair_destruct_2 … EQ2)
254	\| >(pair_destruct_1 ????? EQpc)
255	>(pair_destruct_2 ????? EQpc)
256	@split_elim #x #y #H <H -x y H;
257	>(pair_destruct_1 ????? EQppc)
258	>(pair_destruct_2 ????? EQppc)
259	@split_elim #x #y #H <H -x y H;
260	>EQ0 % ]
261	\| >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
262	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
263	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
264	>external_ram_write_at_stack_pointer %
265	\| change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
266	>EQ0 %
267	\| >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
268	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
269	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
270	>special_function_registers_8051_write_at_stack_pointer %
271	\| >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
272	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
273	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
274	>special_function_registers_8052_write_at_stack_pointer %
275	\| >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
276	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
277	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
278	>p1_latch_write_at_stack_pointer %
279	\| >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
280	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
281	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
282	>p3_latch_write_at_stack_pointer %
283	\| >clock_write_at_stack_pointer whd in ⊢ (??%?)
284	>clock_write_at_stack_pointer whd in ⊢ (???%)
285	>clock_write_at_stack_pointer whd in ⊢ (???%)
286	>clock_write_at_stack_pointer %]
287	(\| ( medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
288	@pair_elim' #fst_5_addr #rest_addr #EQ1
289	@pair_elim' #fst_5_pc #rest_pc #EQ2
290	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
291	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
292	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
293	change in ⊢ (? →??%?) with (execute_1_0 ??)
294	@pair_elim' * #instr #newppc' #ticks #EQn
295	* * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
296	generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
297	@pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
298	@split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
299	@pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
300	change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
301	@split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
302	>get_8051_sfr_set_8051_sfr
303
304	whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
305	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
306	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
307	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
308	generalize in match (refl … (split bool 4 4 pc_bu))
309	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
310	generalize in match (refl … (split bool 3 8 rest_addr))
311	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
312	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
313	generalize in match
314	(refl …
315	(half_add 16 (sigma 〈preamble,instr_list〉 newppc)
316	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
317	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
318	@split_eq_status try %
319	[ change with (? = sigma ? (address_of_word_labels ps label))
320	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
321	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
322	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
323	\|4: (* Jmp *) #label #MAP
324	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
325	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
326	[3: (* long *) #H1 #H2 #EQ %[@1]
327	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
328	change in ⊢ (? → ??%?) with (execute_1_0 ??)
329	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
330	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
331	>H2b >(eq_instruction_to_eq … H2a)
332	generalize in match EQ; -EQ;
333	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
334	cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
335	\|1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
336	generalize in match
337	(refl ?
338	(sub_16_with_carry
339	(sigma 〈preamble,instr_list〉 pol (program_counter … ps))
340	(sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
341	false))
342	cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
343	generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
344	generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
345	#EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
346	generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
347	change in ⊢ (? → ??%?) with (execute_1_0 ??)
348	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
349	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
350	>H2b >(eq_instruction_to_eq … H2a)
351	generalize in match EQ; -EQ;
352	whd in ⊢ (???% → ?);
353	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
354	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
355	generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
356	cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
357	@split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
358	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
359	\| (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
360	generalize in match
361	(refl …
362	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
363	cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
364	generalize in match
365	(refl …
366	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
367	cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
368	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
369	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
370	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
371	change in ⊢ (? →??%?) with (execute_1_0 ??)
372	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
373	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
374	>H2b >(eq_instruction_to_eq … H2a)
375	generalize in match EQ; -EQ;
376	whd in ⊢ (???% → ?);
377	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
378	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
379	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
380	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
381	generalize in match (refl … (split bool 4 4 pc_bu))
382	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
383	generalize in match (refl … (split bool 3 8 rest_addr))
384	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
385	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
386	generalize in match
387	(refl …
388	(half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
389	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
390	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
391	@split_eq_status try %
392	[ change with (? = sigma ?? (address_of_word_labels ps label))
393	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
394	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
395	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
396	\| (* Instruction ) -pi; whd in ⊢ (? → ??%? → ?) ; normalize nodelta;
397	[1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
398	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
399	change in ⊢ (? → ??%?) with (execute_1_0 ??)
400	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
401	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
402	>H2b >(eq_instruction_to_eq … H2a)
403	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
404	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
405	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
406	normalize nodelta; #MAP;
407	[1: change in ⊢ (? → %) with
408	((let 〈result,flags〉 ≝
409	add_8_with_carry
410	(get_arg_8 ? ps false ACC_A)
411	(get_arg_8 ?
412	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
413	false (DIRECT ARG2))
414	? in ?) = ?)
415	[2,3: %]
416	change in ⊢ (???% → ?) with
417	(let 〈result,flags〉 ≝ add_8_with_carry ?((get_arg_8 ? ps false ACC_A)) ?? in ?)
418	>get_arg_8_set_clock
419	[1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
420	[2,4: #abs @⊥ normalize in abs; destruct (abs)
421	\|*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
422	[ change in ⊢ (? → %) with
423	((let 〈result,flags〉 ≝
424	add_8_with_carry
425	(get_arg_8 ? ps false ACC_A)
426	(get_arg_8 ?
427	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
428	false (DIRECT ARG2))
429	? in ?) = ?)
430	>get_arg_8_set_low_internal_ram
431
432	cases (add_8_with_carry ???)
433
434	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
435	#result #flags
436	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
437	\| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
438	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
439	change in ⊢ (? → ??%?) with (execute_1_0 ??)
440	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
441	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
442	>H2b >(eq_instruction_to_eq … H2a)
443	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
444	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
445	[1,2,3,4: cases (half_add ???) #carry #result
446	\| cases (half_add ???) #carry #bl normalize nodelta;
447	cases (full_add ????) #carry' #bu normalize nodelta ]
448	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
449	[5: %
450	\|1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
451	(set_program_counter pseudo_assembly_program ps newppc)
452	(\fst (ticks_of0 〈preamble,instr_list〉
453	(program_counter pseudo_assembly_program ps)
454	(Instruction (INC Identifier (DIRECT ARG))))
455	+clock pseudo_assembly_program
456	(set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
457	[2,3: // ]
458	<(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
459	whd in ⊢ (??%%)
460	cases (split bool 4 4 ARG)
461	#nu' #nl'
462	normalize nodelta
463	cases (split bool 1 3 nu')
464	#bit_1' #ignore'
465	normalize nodelta
466	cases (get_index_v bool 4 nu' ? ?)
467	[ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
468	\|
469	]
470	cases daemon (* EASY CASES TO BE COMPLETED *)
471	qed.

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

Download in other formats:

Original Format