Context Navigation

AssemblyProofSplitSplit.ma @ 2140

Last change on this file since 2140 was 2140, checked in by mulligan, 7 years ago
Done the hardest cases in the main theorem. Just got a few daemons to close...
File size: 16.7 KB

Line
1	include "ASM/AssemblyProofSplit.ma".
2	include "common/LabelledObjects.ma".
3
4	lemma short_jump_cond_ok:
5	∀v1, v2: Word.
6	∀is_possible, offset.
7	〈is_possible, offset〉 = short_jump_cond v1 v2 →
8	is_possible → v2 = add 16 v1 (sign_extension offset).
9	#v1 #v2 #is_possible #offset
10	whd in match short_jump_cond; normalize nodelta
11	@pair_elim #result #flags #sub16_refl
12	@pair_elim #upper #lower #vsplit_refl
13	inversion (get_index' bool ???) #get_index_refl normalize nodelta
14	#relevant destruct(relevant) #relevant
15	[1:
16	@(sub_16_to_add_16_8_1 … flags)
17	\|2:
18	@(sub_16_to_add_16_8_0 … flags)
19	]
20	try assumption >sub16_refl
21	<(eq_bv_eq … relevant)
22	>(vsplit_ok … (sym_eq … vsplit_refl)) %
23	qed.
24
25	lemma absolute_jump_cond_ok:
26	∀v1, v2: Word.
27	∀is_possible, offset, v1_upper, v1_lower.
28	〈is_possible, offset〉 = absolute_jump_cond v1 v2 →
29	〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
30	is_possible → v2 = v1_upper @@ offset.
31	#v1 #v2 #is_possible #offset #v1_upper #v1_lower
32	whd in match absolute_jump_cond; normalize nodelta
33	@pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
34	@pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
35	#relevant destruct(relevant) normalize nodelta #relevant
36	destruct(relevant) #relevant
37	<(vsplit_ok … (sym_eq … vsplit_v2_refl))
38	>(eq_bv_eq … relevant) %
39	qed.
40
41	theorem main_thm:
42	∀M, M': internal_pseudo_address_map.
43	∀program: pseudo_assembly_program.
44	∀program_in_bounds: \|\snd program\| ≤ 2^16.
45	∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
46	∀is_well_labelled: is_well_labelled_p (\snd program).
47	∀sigma: Word → Word.
48	∀policy: Word → bool.
49	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
50	∀ps: PseudoStatus program.
51	∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < \|\snd program\|.
52	next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
53	∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
54	status_of_pseudo_status M' …
55	(execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
56	#M #M' * #preamble #instr_list #program_in_bounds #addr_of
57	#is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
58	letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
59	change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
60	generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
61	@pair_elim #labels #costs #create_label_cost_refl normalize nodelta
62	@pair_elim #assembled #costs' #assembly_refl normalize nodelta
63	lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
64	@pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
65	@(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
66	@(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
67	whd in match execute_1_pseudo_instruction; normalize nodelta
68	whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
69	lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
70	lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
71	[1: assumption \|2: assumption] >create_label_cost_refl
72	#X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
73	[1: >fetch_pseudo_refl %]
74	#assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
75	generalize in match assm1; -assm1 -assm2 -assm3
76	normalize nodelta
77	inversion pi
78	[2,3:
79	#arg #_
80	(* XXX: we first work on sigma_increment_commutation *)
81	#sigma_increment_commutation
82	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
83	(* XXX: we work on the maps *)
84	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
85	(* XXX: we assume the fetch_many hypothesis *)
86	#fetch_many_assm
87	(* XXX: we give the existential *)
88	%{0}
89	whd in match (execute_1_pseudo_instruction0 ?????);
90	(* XXX: work on the left hand side of the equality *)
91	whd in ⊢ (??%?);
92	@split_eq_status try %
93	/demod/ >add_commutative <add_zero % (CSC: auto not working, why? )
94	\|6: (* Mov *)
95	#arg1 #arg2 #_
96	(* XXX: we first work on sigma_increment_commutation *)
97	#sigma_increment_commutation
98	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
99	(* XXX: we work on the maps *)
100	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
101	(* XXX: we assume the fetch_many hypothesis *)
102	#fetch_many_assm
103	(* XXX: we give the existential *)
104	%{1}
105	whd in match (execute_1_pseudo_instruction0 ?????);
106	(* XXX: work on the left hand side of the equality *)
107	whd in ⊢ (??%?); whd in match (program_counter ???);
108	(* XXX: execute fetches some more *)
109	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
110	whd in fetch_many_assm;
111	>EQassembled in fetch_many_assm;
112	cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
113	#eq_instr
114	#fetch_many_assm whd in fetch_many_assm;
115	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
116	destruct whd in ⊢ (??%?);
117	(* XXX: now we start to work on the mk_PreStatus equality *)
118	(* XXX: lhs *)
119	change with (set_arg_16 ????? = ?)
120	>set_program_counter_mk_Status_commutation
121	>set_clock_mk_Status_commutation
122	>set_arg_16_mk_Status_commutation
123	(* XXX: rhs *)
124	change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
125	>set_program_counter_mk_Status_commutation
126	>set_clock_mk_Status_commutation
127	>set_arg_16_mk_Status_commutation in ⊢ (???%);
128	(* here we are *)
129	@split_eq_status try %
130	[1:
131	assumption
132	\|2:
133	@special_function_registers_8051_set_arg_16 %
134	]
135	\|1: (* Instruction *)
136	#instr #pi_refl #EQP #EQnext #fetch_many_assm
137	@(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
138	ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
139	EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
140	(λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
141	(refl …) ? (refl …))
142	[1,2:
143	assumption
144	\|3:
145	%
146	\|4:
147	>fetch_pseudo_refl @pi_refl
148	\|5:
149	<EQP %
150	\|6:
151	>assembly_refl assumption
152	\|7:
153	<EQassembled assumption
154	]
155	\|4: (* Jmp *)
156	#arg1 #pi_refl
157	(* XXX: we first work on sigma_increment_commutation *)
158	whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
159	whd in match (expand_pseudo_instruction ??????);
160	inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
161	inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
162	[2:
163	inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
164	inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
165	]
166	#sigma_increment_commutation
167	normalize in sigma_increment_commutation:(???(???(??%)));
168	(* XXX: we work on the maps *)
169	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
170	(* XXX: we assume the fetch_many hypothesis *)
171	* #fetch_refl #fetch_many_assm
172	(* XXX: we give the existential *)
173	%{1}
174	(* XXX: work on the left hand side of the equality *)
175	whd in ⊢ (??%?); whd in match (program_counter ???);
176	(* XXX: execute fetches some more *)
177	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
178	whd in fetch_many_assm;
179	>EQassembled in fetch_refl; #fetch_refl <fetch_refl
180	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
181	whd in ⊢ (??%%);
182	(* XXX: now we start to work on the mk_PreStatus equality *)
183	(* XXX: lhs *)
184	(* XXX: rhs *)
185	(* here we are *)
186	@split_eq_status try % /demod nohyps/
187	[1,3,4:
188	change with (add ???) in match (\snd (half_add ???));
189	whd in match execute_1_pseudo_instruction0; normalize nodelta
190	/demod nohyps/ >set_clock_set_program_counter
191	>program_counter_set_program_counter
192	whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
193	lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
194	normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
195	[1:
196	>EQnewpc
197	inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
198	@sym_eq
199	>EQlookup_labels in mjc_refl; #mjc_refl
200	@(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
201	>(andb_true_l … mj_possible_refl) @I
202	\|3:
203	>EQlookup_labels normalize nodelta %
204	\|5:
205	>EQnewpc
206	inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
207	@sym_eq
208	>EQlookup_labels in sjc_refl; #sjc_refl
209	>(pair_destruct_2 ????? (sym_eq … half_add_refl))
210	@(short_jump_cond_ok ???? (sym_eq … sjc_refl))
211	>(andb_true_l … sj_possible_refl) @I
212	]
213	whd in is_well_labelled_witness;
214	@(is_well_labelled_witness ? ppc ppc_in_bounds pi)
215	try (>fetch_pseudo_refl %)
216	>pi_refl %
217	\|2:
218	whd in ⊢ (??(?%%)%);
219	cases (bitvector_11_cases address)
220	* * * * * * #b4 * #b5
221	* #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
222	normalize in match (fetch ??); <plus_n_Sm @eq_f
223	@commutative_plus
224	]
225	\|5: (* Call *)
226	#arg1 #pi_refl
227	(* XXX: we first work on sigma_increment_commutation *)
228	whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
229	whd in match (expand_pseudo_instruction ??????);
230	whd in match (execute_1_pseudo_instruction0 ?????);
231	inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
232	inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
233	@pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
234	@pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
235	@pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
236	#sigma_increment_commutation
237	normalize in sigma_increment_commutation:(???(???(??%)));
238	(* XXX: we work on the maps *)
239	whd in ⊢ (??%? → ?);
240	@pair_elim #callM #accM #Mrefl
241	@Some_Some_elim #map_refl_assm <map_refl_assm
242	(* XXX: we assume the fetch_many hypothesis *)
243	* #fetch_refl #fetch_many_assm
244	(* XXX: we give the existential *)
245	%{1}
246	(* XXX: work on the left hand side of the equality *)
247	whd in ⊢ (??%?); whd in match (program_counter ???);
248	(* XXX: execute fetches some more *)
249	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
250	whd in fetch_many_assm;
251	>EQassembled in fetch_refl; #fetch_refl <fetch_refl
252	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
253	whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
254	normalize in match (length ? (assembly1 …)) in EQnewpc;
255	normalize nodelta
256	[1:
257	@(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
258	try /demod nohyps/ [1: %]
259	@pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
260	@(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
261	try /demod nohyps/ [1: %]
262	@pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
263	@split_eq_status try /demod nohyps/ try %
264	[1,2:
265	(* XXX: need the commented out axioms from AssemblyProof.ma *)
266	cases daemon
267	\|3:
268	lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
269	change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
270	#relevant <(relevant arg1)
271	[2:
272	@(is_well_labelled_witness … ppc_in_bounds pi)
273	[1:
274	>fetch_pseudo_refl %
275	\|2:
276	>pi_refl %
277	]
278	\|1:
279	whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
280	>EQlookup_labels normalize nodelta
281	@vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
282	>fst_5_rest_refl normalize nodelta
283	@vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
284	#pair_true_refl destruct(pair_true_refl)
285	<EQnewpc in fst_5_rest_pc_refl;
286	lapply pc_bu_bl_refl' -pc_bu_bl_refl'
287	>program_counter_set_8051_sfr >set_clock_set_program_counter
288	>program_counter_set_program_counter #relevant2
289	<(vsplit_ok ?????? (sym_eq … relevant2))
290	<(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
291	>(vector_associative_append bool 5 3 8) #relevant3
292	>(? : fiv = fst_5_addr)
293	[1:
294	%
295	\|2:
296	cases daemon
297	]
298	]
299	\|4:
300	>set_program_counter_mk_Status_commutation in ⊢ (???%);
301	>special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
302	(* XXX: require set_8051_sfr_write_at_stack_pointer and
303	special_function_registers_8051_set_8051_sfr
304	*)
305	cases daemon
306	\|5,6,7:
307	>set_program_counter_mk_Status_commutation in ⊢ (???%);
308	(* XXX: similar to above but for 8052
309	*)
310	cases daemon
311	\|8:
312	whd in match (ticks_of_instruction ?);
313	cut(\snd (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
314	[1: //
315	\|2:
316	normalize in match (assembly1 ?);
317	@(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
318	\|3:
319	#fetch_2_refl >fetch_2_refl >commutative_plus %
320	]
321	]
322	\|2:
323	@(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
324	try /demod nohyps/ [1: %]
325	@pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
326	@(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
327	try /demod nohyps/ [1: %]
328	@split_eq_status try /demod nohyps/ try %
329	[1:
330	cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
331	[1:
332	>(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
333	>set_clock_set_program_counter >program_counter_set_program_counter
334	>add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
335	\|2:
336	#relevant cases daemon
337	(* XXX: need axioms *)
338	]
339	\|2:
340	cases daemon (* XXX: need axioms from assembly.ma *)
341	\|3:
342	change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
343	lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
344	#relevant <(relevant arg1)
345	[1:
346	>EQlookup_labels %
347	\|2:
348	@(is_well_labelled_witness … ppc_in_bounds pi)
349	[1:
350	>fetch_pseudo_refl %
351	\|2:
352	>pi_refl %
353	]
354	]
355	\|4:
356	>set_program_counter_mk_Status_commutation in ⊢ (???%);
357	>special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
358	(* XXX: require set_8051_sfr_write_at_stack_pointer and
359	special_function_registers_8051_set_8051_sfr
360	*)
361	cases daemon
362	\|5,6,7:
363	>set_program_counter_mk_Status_commutation in ⊢ (???%);
364	(* XXX: similar to above but for 8052
365	*)
366	cases daemon
367	]
368	]
369	]
370	qed.

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

Download in other formats:

Original Format