Context Navigation

toCminorCorrectness.ma @ 2672

Last change on this file since 2672 was 2667, checked in by garnier, 8 years ago
Clight to Cminor, statements: some cases down. Subset of the simulation relation defined and seems to work. Some cosmetic changes in toCminorCorrectnessExpr in order to clarify things in toCminorCorrectness.
File size: 30.3 KB

Line
1	include "Clight/toCminor.ma".
2	include "Clight/CexecInd.ma".
3	include "common/Globalenvs.ma".
4	include "Clight/memoryInjections.ma".
5	include "Clight/Clight_abstract.ma".
6	include "Cminor/Cminor_abstract.ma".
7
8	(* Expr simulation. Contains important definitions for statements, too. *)
9	include "Clight/toCminorCorrectnessExpr.ma".
10
11
12	(* When we characterise the local Clight variables, those that are stack
13	allocated are given disjoint regions of the stack. *)
14
15	lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
16	characterise_vars globals f = 〈vartypes, stacksize〉 →
17	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
18	∀id',n',ty'. id ≠ id' →
19	lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
20	n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
21	#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
22	whd in ⊢ (??%? → ?);
23	generalize in match vartypes; -vartypes
24	generalize in match stacksize; -stacksize
25	elim (args@vars)
26	[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
27	elim globals in L;
28	[ normalize #L destruct
29	\| * * #id' #r #ty' #tl #IH
30	whd in match (foldr ?????);
31	#L cases (lookup_add_cases ??????? L)
32	[ * #E1 #E2 destruct
33	\| @IH
34	]
35	]
36	\| * #id1 #ty1 #tl #IH #stacksize #vartypes
37	whd in match (foldr ?????);
38	(* Avoid writing out the definition again *)
39	letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
40	lapply (refl ? ih) whd in match ih; -ih
41	cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
42	#vartypes' #stack' #FOLD #IH
43	whd in ⊢ (??(match % with [_⇒?])? → ?);
44	cases (orb ??)
45	#CHAR whd in CHAR:(??%?); destruct
46	#L cases (lookup_add_cases ??????? L)
47	[ 1,3: * #E1 #E2 destruct
48	#id' #n' #ty' #NE >lookup_add_miss /2/
49	#L' %1 -L -IH
50	generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
51	generalize in match stack'; -stack'
52	elim tl
53	[ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
54	elim globals in L';
55	[ normalize #E destruct
56	\| * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
57	#L cases (lookup_add_cases ??????? L)
58	[ * #E1 #E2 destruct
59	\| @IH
60	]
61	]
62	\| * #id2 #ty2 #tl2 #IH #stack' #vartypes'
63	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
64	#vartypes2 #stack2 #IH
65	whd in ⊢ (??%? → ?);
66	cases (orb ??)
67	[ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
68	[ * #E1 #E2 destruct //
69	\| #L'' lapply (IH ?? (refl ??) L'') /2/
70	]
71	\| #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
72	[ * #E1 #E2 destruct
73	\| #L'' lapply (IH ?? (refl ??) L'') /2/
74	]
75	]
76	]
77	\| -L #L #id' #n' #ty' #NE #L'
78	cases (lookup_add_cases ??????? L')
79	[ * #E1 #E2 destruct
80	%2 -IH -L'
81	generalize in match vartypes' in FOLD L; -vartypes'
82	generalize in match stack'; -stack'
83	elim tl
84	[ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
85	elim globals in L;
86	[ normalize #E destruct
87	\| * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
88	#L cases (lookup_add_cases ??????? L)
89	[ * #E1 #E2 destruct
90	\| @IH
91	]
92	]
93	\| * #id1 #ty1 #tl1 #IH #stack' #vartypes'
94	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
95	#vartypes2 #stack2 #IH
96	whd in ⊢ (??%? → ?);
97	cases (orb ??)
98	#E whd in E:(??%?); destruct
99	#L cases (lookup_add_cases ??????? L)
100	[ 1,3: * #E1 #E2 destruct //
101	\| 2,4: #L' lapply (IH ?? (refl ??) L') /2/
102	]
103	]
104	\| @(IH … (refl ??) L … NE)
105	]
106	\| -L #L #id' #n' #ty' #NE #L'
107	cases (lookup_add_cases ??????? L')
108	[ * #E1 #E2 destruct
109	\| @(IH … (refl ??) L … NE)
110	]
111	]
112	] qed.
113
114	(* And everything is in the stack frame. *)
115
116	lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
117	characterise_vars globals f = 〈vartypes, stacksize〉 →
118	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
119	n + sizeof ty ≤ stacksize.
120	#globals * #ret #args #vars #body whd in match (characterise_vars ??);
121	elim (args@vars)
122	[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
123	whd in FOLD:(??%?); destruct elim globals in L;
124	[ #E normalize in E; destruct
125	\| * * #id' #r' #ty' #tl' #IH
126	whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
127	[ * #E1 #E2 destruct
128	\| @IH
129	]
130	]
131	\| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
132	whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
133	#vartypes' #stackspace' #IH
134	whd in ⊢ (??(match % with [_⇒?])? → ?);
135	cases (orb ??) whd in ⊢ (??%? → ?);
136	#E destruct #L cases (lookup_add_cases ??????? L)
137	[ 1,3: * #E1 #E2 destruct //
138	\| 2,4: #L' lapply (IH … (refl ??) L') /2/
139	]
140	] qed.
141
142
143
144	(* Put knowledge that Globals are global into a more useful form than the
145	one used for the invariant. *)
146	(* XXX superfluous lemma ? Commenting it for now.
147	if not superfluous : move to toCminorCorrectnessExpr.ma, after
148	[characterise_vars_localid] *)
149	(*
150	lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
151	characterise_vars globals f = 〈vartypes, stacksize〉 →
152	∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
153	Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
154	¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
155	#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
156	cases (characterise_vars_src … CHAR id ?)
157	[ * #r' * #ty' >L
158	* #E1 destruct (E1) #EX
159	%
160	[ @EX
161	\| % #EX' cases (characterise_vars_localid … CHAR EX')
162	#ty' whd in ⊢ (% → ?); >L *
163	]
164	\| * #ty' whd in ⊢ (% → ?); >L *
165	\| whd >(opt_eq_from_res ???? L) % #E destruct
166	] qed. *)
167
168	(* Show how the global environments match up. *)
169
170	lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
171	map_partial_All A B P f l H = OK ? l' →
172	All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
173	#A #B #P #f #l
174	elim l
175	[ #H #l' #MAP normalize in MAP; destruct //
176	\| #h #t #IH * #p #H #l'
177	whd in ⊢ (??%? → ?);
178	lapply (refl ? (f h p)) whd in match (proj1 ???);
179	cases (f h p) in ⊢ (???% → %);
180	[ #b #E #MAP cases (bind_inversion ????? MAP)
181	#tl' * #MAP' #E' normalize in E'; destruct
182	% [ %{p} @E \| @IH [ @H \| @MAP' ] ]
183	\| #m #_ #X normalize in X; destruct
184	]
185	] qed.
186
187
188	definition clight_cminor_matching : clight_program → matching ≝
189	λp.
190	let tmpuniverse ≝ universe_for_program p in
191	let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
192	let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
193	let globals ≝ fun_globals @ var_globals in
194	mk_matching
195	?? (list init_data × type) (list init_data)
196	(λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
197	(λv,w. \fst v = w).
198
199	lemma clight_to_cminor_varnames : ∀p,p'.
200	clight_to_cminor p = OK ? p' →
201	prog_var_names … p = prog_var_names … p'.
202	* #vars #fns #main * #vars' #fns' #main'
203	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
204	whd in E:(??%%); destruct
205	-MAP normalize
206	elim vars
207	[ //
208	\| * * #id #r * #d #t #tl #IH normalize >IH //
209	] qed.
210
211	lemma clight_to_cminor_matches : ∀p,p'.
212	clight_to_cminor p = OK ? p' →
213	match_program (clight_cminor_matching p) p p'.
214	* #vars #fns #main * #vars' #fns' #main'
215	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
216	whd in E:(??%%); destruct
217	%
218	[ -MAP whd in match (m_V ?); whd in match (m_W ?);
219	elim vars
220	[ //
221	\| * * #id #r * #init #ty #tl #IH %
222	[ % //
223	\| @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
224	]
225	]
226	\| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
227	* #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
228	normalize in E; destruct
229	<(clight_to_cminor_varnames … TO)
230	% whd
231	% [2: % [2: @TRANSF \| skip ] \| skip ]
232	\| %
233	] qed.
234
235
236	(* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
237	for easier reference.
238	lemma eval_expr_sim :
239	(* [cl_cm_inv] maps CL globals to CM globals, including functions *)
240	∀cl_cm_inv : clight_cminor_inv.
241	(* current function (defines local environment) *)
242	∀f : function.
243	∀data : clight_cminor_data f cl_cm_inv.
244	(* clight expr to cminor expr *)
245	(∀(e:expr).
246	∀(e':CMexpr (typ_of_type (typeof e))).
247	∀Hexpr_vars.
248	translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
249	∀cl_val,trace,Hyp_present.
250	exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 →
251	∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
252	value_eq (E ?? data) cl_val cm_val) ∧
253	(* clight /lvalue/ to cminor /expr/ *)
254	(∀ed,ty.
255	∀(e':CMexpr ASTptr).
256	∀Hexpr_vars.
257	translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
258	∀cl_blo,cl_off,trace,Hyp_present.
259	exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
260	∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
261	value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
262	*)
263
264	definition foo ≝ 3.
265
266	(* relate Clight continuations and Cminor ones. *)
267	inductive clight_cminor_cont_rel :
268	∀INV: clight_cminor_inv. (* stuff on global variables and functions (matching between CL and CM) *)
269	∀cl_f: function. (* current Clight function *)
270	internal_function → (* current Cminor function *)
271	clight_cminor_data cl_f INV → (* data for the current stack frame in CL and CM *)
272	option typ → (* optional target type - uniform over a given function *)
273	cl_cont → (* CL cont *)
274	cm_cont → (* CM cont *)
275	Prop ≝
276	\| ClCm_cont_stop:
277	∀INV, cl_f, cm_f, frame_data, target_type.
278	clight_cminor_cont_rel INV cl_f cm_f frame_data target_type Kstop Kend
279	\| ClCm_cont_seq:
280	∀INV, cl_f, cm_f, frame_data, target_type.
281	∀cl_s: statement.
282	∀cm_s: stmt.
283	∀cl_k': cl_cont.
284	∀cm_k': cm_cont.
285	∀stmt_univ, stmt_univ'.
286	∀lbl_univ, lbl_univ'.
287	∀lbls.
288	∀flag.
289	∀Htranslate_inv.
290	translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
291	clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
292	clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
293	\| ClCm_cont_while:
294	(* Inductive family parameters *)
295	∀INV, cl_f, cm_f, frame_data, target_type.
296
297	(* sub-continuations *)
298	∀cl_k': cl_cont.
299	∀cm_k': cm_cont.
300
301	(* elements of the source while statement *)
302	∀sz,sg.
303	∀cl_cond_desc.
304	∀cl_body.
305
306	(* elements of the converted while statement *)
307	∀cm_cond: CMexpr (ASTint sz sg).
308	∀cm_body.
309	∀entry,exit: identifier Label.
310
311	(* universes used to generate fresh labels and variables *)
312	∀stmt_univ, stmt_univ'.
313	∀lbl_univ, lbl_univ', lbl_univ''.
314	∀lbls: lenv.
315	∀Htranslate_inv.
316
317	(* relate CL and CM expressions *)
318	∀Hexpr_vars.
319	translate_expr (alloc_type ?? frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
320
321	(* Parameters and results to find_label_always *)
322	∀sInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).
323	∀Hinv.
324
325	(* Specify how the labels for the while-replacing gotos are produced *)
326	mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
327	translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
328	find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env ?? frame_data) sInv I =
329	«〈St_label entry
330	(St_seq
331	(St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
332	(St_label exit St_skip)), cm_k'〉, Hinv» →
333	clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
334	clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
335
336
337	(* The type of maps from labels to Clight continuations *)
338	(* definition label_map ≝ identifier_map SymbolTag cont. *)
339
340	(* Definition of the simulation relation on states. The orders of the parameters is dictated by
341	* the necessity of performing an inversion on the continuation sim relation without having to
342	* play the usual game of lapplying all previous dependent arguments. *)
343	inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
344	\| CMR_normal :
345	(* Relates globals to globals and functions to functions. *)
346	∀INV: clight_cminor_inv.
347
348	(* ---- Statements ---- *)
349	∀cl_s: statement. (* Clight statement *)
350	∀cm_s: stmt. (* Cminor statement *)
351
352	(* ---- Continuations ---- *)
353	∀cl_k: cl_cont. (* Clight continuation *)
354	∀cm_k: cm_cont. (* Cminor continuation *)
355	∀cm_st: stack. (* Cminor stack *)
356
357	∀cl_f: function. (* Clight enclosing function *)
358	∀cm_f: internal_function. (* enclosing function *)
359	∀frame_data: clight_cminor_data cl_f INV.
360	(∀alloctype: var_types.) (* map from var to alloc type *)
361	∀rettyp. (* return type of the function *)
362
363	(* ---- Relate Clight continuation to Cminor continuation ---- *)
364	clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k →
365
366	(* ---- Other Cminor variables ---- *)
367	∀fInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f). (* Cminor invariants *)
368	∀sInv: stmt_inv cm_f (cm_env ?? frame_data) cm_s.
369	∀kInv: cont_inv cm_f (cm_env ?? frame_data) cm_k.
370
371	(* ---- Relate return type variable to actual return type ---- *)
372	rettyp = opttyp_of_type (fn_return cl_f) →
373
374	(* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
375
376	(* ---- relate Clight and Cminor functions ---- *)
377	∀func_univ: universe SymbolTag.
378	∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
379	∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
380	translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
381
382	(* ---- relate Clight and Cminor statements ---- *)
383	∀stmt_univ,stmt_univ': tmpgen (alloc_type ?? frame_data).
384	∀lbl_univ,lbl_univ': labgen.
385	∀lbls: lenv.
386	∀flag: convert_flag.
387	∀Htranslate_inv.
388	translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
389
390	clight_cminor_rel INV
391	(ClState cl_f cl_s cl_k (cl_env ?? frame_data) (cl_m ?? frame_data))
392	(CmState cm_f cm_s (cm_env ?? frame_data) fInv sInv (cm_m ?? frame_data) (stackptr ?? frame_data) cm_k kInv cm_st).
393
394	lemma invert_assert :
395	∀b. ∀P. assert b P → b = true ∧ P.
396	* #P whd in ⊢ (% → ?); #H
397	[ @conj try @refl @H
398	\| @False_ind @H ]
399	qed.
400
401	lemma res_to_io :
402	∀A,B:Type[0]. ∀C.
403	∀x: res A. ∀y.
404	match x with
405	[ OK v ⇒ Value B C ? v
406	\| Error m ⇒ Wrong … m ] = return y →
407	x = OK ? y.
408	#A #B #C *
409	[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
410	\| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
411	qed.
412
413
414	(* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *)
415
416	(* Conjectured simulation results
417
418	We split these based on the start state:
419
420	1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
421	normal steps in Cminor;
422	2. call and return steps are simulated by a call/return step plus [m] normal
423	steps (to copy stack allocated parameters / results); and
424	3. lone cost label steps are simulates by a lone cost label step
425
426	These should allow us to maintain enough structure to identify the Cminor
427	subtrace corresponding to a measurable Clight subtrace.
428	*)
429
430	definition clight_normal : Clight_state → bool ≝
431	λs. match Clight_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
432
433	definition cminor_normal : Cminor_state → bool ≝
434	λs. match Cminor_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
435
436
437	lemma clight_cminor_normal :
438	∀INV:clight_cminor_inv.
439	∀s1,s1',s2,tr.
440	clight_cminor_rel INV s1 s1' →
441	clight_normal s1 = true →
442	¬ Clight_labelled s1 →
443	∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
444	∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
445	tr = tr' ∧
446	clight_cminor_rel INV s2 s2'
447	).
448	#INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld
449	inversion Hstate_rel
450	#INV' #cl_s
451	(* case analysis on Clight statement *)
452	cases cl_s
453	[ 1: \| 2: #lhs #rhs \| 3: #retv #func #args \| 4: #stm1 #stm2 \| 5: #cond #iftrue #iffalse \| 6: #cond #body
454	\| 7: #cond #body \| 8: #init #cond #step #body \| 9,10: \| 11: #retval \| 12: #cond #switchcases \| 13: #lab #body
455	\| 14: #lab \| 15: #cost #body ]
456	[ 1: (* Skip *)
457	#cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
458	(* case analysis on continuation *)
459	inversion Hcont_rel
460	[ (* Kstop continuation *)
461	(* simplifying the goal using outcome of the inversion *)
462	#kINV #kcl_f #kcm_f #kframe_data #ktarget_type #Heq_INV
463	#Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_
464	(* get rid of jmeqs and destruct *)
465	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
466	lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
467	destruct (Heq_INV Heq_cl_f)
468	lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
469	lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
470	lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
471	lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
472	lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
473	destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)
474	(* introduce everything *)
475	#fInv #sInv #kInv
476	#Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
477	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
478	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
479	#Hreturn_ok #Hlabel_wf
480	(* reduce statement translation function *)
481	whd in ⊢ ((??%?) → ?);
482	#Heq_translate
483	(* In this simple case, trivial translation *)
484	destruct (Heq_translate)
485	#Heq_INV' #Heq_s1 #Heq_s1'
486	lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
487	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
488	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
489	destruct (Heq_INV' Heq_s1 Heq_s1') #_
490	(* unfold the clight execution *)
491	%{0}
492	whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??);
493	inversion (fn_return kcl_f) normalize nodelta
494	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
495	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
496	#Hfn_return
497	whd in ⊢ (% → ?);
498	@False_ind
499	\| (* KSeq continuation *)
500	#kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
501	#kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
502	* * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
503	#kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
504	#Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_
505	(* get rid of jmeqs and destruct *)
506	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
507	lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
508	destruct (Heq_INV Heq_cl_f)
509	lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
510	lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
511	lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
512	lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
513	lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
514	destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)
515	#fInv #sInv #kInv #Hktarget_type
516	#func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
517	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
518	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
519	#Hreturn_ok #Hlabel_wf
520	(* reduce translation function and eliminate result *)
521	(* In this simple case, trivial translation *)
522	whd in ⊢ ((??%?) → ?); #Heq_translate
523	destruct (Heq_translate)
524	#Heq_INV' #Heq_s1 #Heq_s1'
525	lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
526	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
527	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
528	(* unfold the clight execution *)
529	%{0}
530	whd in ⊢ (% → ?); #Hassert
531	cases (invert_assert ?? Hassert) -Hassert #Hclight_class
532	cases (andb_inversion … Hclight_class) -Hclight_class
533	#_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
534	%{0} whd in ⊢ %; @conj try @refl
535	(* close simulation *)
536	%1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
537	Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
538	[ 3: @kHeq_translate \| assumption ]
539	\| (* Kwhile continuation *)
540	#kINV #kcl_f #kcm_f #kframe_data #ktarget_type
541	#kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
542	#kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
543	#klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
544	* * * * #kHentry_declared * * * *
545	* * * #kHcond_vars_declared * * * *
546	* * * #kHbody_inv * * *
547	whd in ⊢ (% → ?); #kHentry_declared'
548	* * * * * * * * *
549	whd in ⊢ (% → ?); #kHexit_declared *
550	* * * *
551	#kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
552	#Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
553	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
554	lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
555	destruct (Heq_INV Heq_cl_f)
556	lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
557	lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
558	lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
559	lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
560	lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
561	destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
562	(* introduce state relation contents *)
563	#fInv #sInv * whd in ⊢ (% → ?); * *
564	whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
565	#Heq_rettyp
566	#func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
567	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
568	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
569	#Hreturn_ok #Hlabel_wf
570	(* reduce translation function and eliminate result *)
571	(* In this simple case, trivial translation *)
572	whd in ⊢ ((??%?) → ?); #Heq_translate
573	destruct (Heq_translate)
574	#Heq_INV' #Heq_s1 #Heq_s1'
575	lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
576	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
577	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
578	(* unfold the clight execution *)
579	%{1} whd in ⊢ (% → ?); #Hawait
580	cases (await_value_bind_inv … Hawait) -Hawait
581	* #cl_val #cl_trace * #Hexec_cond #Hawait
582	cases (await_value_bind_inv … Hawait) -Hawait
583	#cond_outcome * #Hcond_outcome
584	cases (eval_expr_sim … kframe_data) #Hsim_expr #_
585	(* use simulation lemma on expressions *)
586	lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
587	whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
588	#Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
589	* [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
590	* [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
591	* #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
592	normalize nodelta #Hi_eq
593	* #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
594	cases (invert_assert … Hassert) -Hassert #Handb
595	cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
596	whd in ⊢ (% → ?); #Heq destruct (Heq)
597	[ %{5} whd whd in ⊢ (??%?); normalize nodelta
598	>kHfind_label -kHfind_label normalize nodelta
599	whd in match (proj1 ???);
600	whd in match (proj2 ???);
601	whd whd in ⊢ (??%?); normalize nodelta
602	>Hexec_cond_cm normalize nodelta
603	whd in match (m_bind ?????);
604	>(value_eq_int_inversion … Hvalue_eq)
605	whd in match (eval_bool_of_val ?); normalize nodelta
606	<Hi_eq normalize nodelta
607	whd @conj [ normalize >append_nil try @refl ]
608	whd in match (proj1 ???);
609	whd in match (proj2 ???);
610	whd whd in ⊢ (??%?); normalize nodelta
611	%{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
612	??????? kHeq_translate}
613	\| %{6} whd whd in ⊢ (??%?); normalize nodelta
614	>kHfind_label -kHfind_label normalize nodelta
615	whd in match (proj1 ???);
616	whd in match (proj2 ???);
617	whd whd in ⊢ (??%?); normalize nodelta
618	>Hexec_cond_cm normalize nodelta
619	whd in match (m_bind ?????);
620	>(value_eq_int_inversion … Hvalue_eq)
621	whd in match (eval_bool_of_val ?); normalize nodelta
622	<Hi_eq normalize nodelta
623	whd @conj [ normalize >append_nil >append_nil try @refl ]
624	whd in match (proj1 ???);
625	whd in match (proj2 ???);
626	whd whd in ⊢ (??%?); normalize nodelta
627	%{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
628	try assumption
629	[ @conj try @conj try @conj try @conj //
630	\| @refl ]
631	]
632	(\| TODO: other continuations )
633	]
634	\| 2: (* Assign *)
635	#cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
636	#fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
637	#Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
638	* * * * #Hstmt_inv_cm #Huseless_hypothesis
639	#Htmps_preserved #Hreturn_ok #Hlabel_wf
640	(* case-split on lhs in order to reduce lvalue production in Cminor *)
641	cases lhs #lhs_ed #lhs_ty
642	cases lhs_ed
643	(* intro expr contents *)
644	[ #sz #i \| #var_id \| #e1 \| #e1 \| #op #e1 \|#op #e1 #e2 \| #cast_ty #e1
645	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
646	[ 2: #Htranslate_statement
647	cases (bind_inversion ????? Htranslate_statement)
648	* #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
649	cases (bind_inversion ????? Htranslate_statement')
650	#lhs_dest * #Htranslate_lhs
651	cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
652	#alloctype * #type_of_var * #Hlookup_var_success
653	cases alloctype in Hlookup_var_success;
654	normalize nodelta
655	[ 1: (* Global *) #r
656	#Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
657	destruct (Hlhs_dest_eq) normalize nodelta
658	whd in match (proj1 ???); whd in match (proj2 ???);
659	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
660	#Heq_INV #Heq_s1 #Heq_s1'
661	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
662	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
663	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
664	destruct (Heq_INV Heq_s1 Heq_s1') #_
665	%{1} whd in ⊢ (% → ?); #Hawait
666	cases (await_value_bind_inv … Hawait) -Hawait
667	* * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
668	#Hexec_lvalue
669	lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
670	#Hawait
671	cases (await_value_bind_inv … Hawait) -Hawait
672	* #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
673	cases (await_value_bind_inv … Hawait) -Hawait
674	#mem_after_store * #Hstore_value #Hawait
675	lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
676	-Htranslate_statement' -Htranslate_statement
677	cases (invert_assert … Hawait) -Hawait #Handb
678	cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait
679	(* TODO: use the memory injection to handle the store,
680	use INV contents to match up CL global with CM one.
681	Note to self: globals should be exactly matched in CL and CM,
682	maybe memory_injection is not useful in this particular case,
683	only in Stack and Local cases.
684	* *)
685	@cthulhu
686	\| 2: (* Stack *) #n @cthulhu
687	\| 3: (* Local *) @cthulhu
688	]
689	\| : ( memdest *) @cthulhu ]
690	\| *: @cthulhu
691	] qed.
692
693	axiom clight_cminor_call_return :
694	∀INV:clight_cminor_inv.
695	∀s1,s1',s2,tr.
696	clight_cminor_rel INV s1 s1' →
697	match Clight_classify s1 with [ cl_call ⇒ true \| cl_return ⇒ true \| _ ⇒ false ] →
698	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
699	∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
700	tr = tr' ∧
701	clight_cminor_rel INV s2 s2'
702	).
703
704	axiom clight_cminor_cost :
705	∀INV:clight_cminor_inv.
706	∀s1,s1',s2,tr.
707	clight_cminor_rel INV s1 s1' →
708	Clight_labelled s1 →
709	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
710	after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
711	tr = tr' ∧
712	clight_cminor_rel INV s2 s2'
713	).
714
715	axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
716	clight_to_cminor cl_program = OK ? cm_program →
717	make_initial_state ?? clight_fullexec cl_program = OK ? s →
718	make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
719	∃INV. clight_cminor_rel INV s s'.

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

Download in other formats:

Original Format