Context Navigation

toCminorCorrectness.ma @ 2745

Last change on this file since 2745 was 2737, checked in by garnier, 8 years ago
Commit of current proof state for Clight to Cminor translation.
File size: 53.4 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	include "common/Measurable.ma".
8
9	(* Expr simulation. Contains important definitions for statements, too. *)
10	include "Clight/toCminorCorrectnessExpr.ma".
11
12	(* When we characterise the local Clight variables, those that are stack
13	allocated are given disjoint regions of the stack. *)
14	lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
15	characterise_vars globals f = 〈vartypes, stacksize〉 →
16	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
17	∀id',n',ty'. id ≠ id' →
18	lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
19	n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
20	#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
21	whd in ⊢ (??%? → ?);
22	generalize in match vartypes; -vartypes
23	generalize in match stacksize; -stacksize
24	elim (args@vars)
25	[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
26	elim globals in L;
27	[ normalize #L destruct
28	\| * * #id' #r #ty' #tl #IH
29	whd in match (foldr ?????);
30	#L cases (lookup_add_cases ??????? L)
31	[ * #E1 #E2 destruct
32	\| @IH
33	]
34	]
35	\| * #id1 #ty1 #tl #IH #stacksize #vartypes
36	whd in match (foldr ?????);
37	(* Avoid writing out the definition again *)
38	letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
39	lapply (refl ? ih) whd in match ih; -ih
40	cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
41	#vartypes' #stack' #FOLD #IH
42	whd in ⊢ (??(match % with [_⇒?])? → ?);
43	cases (orb ??)
44	#CHAR whd in CHAR:(??%?); destruct
45	#L cases (lookup_add_cases ??????? L)
46	[ 1,3: * #E1 #E2 destruct
47	#id' #n' #ty' #NE >lookup_add_miss /2/
48	#L' %1 -L -IH
49	generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
50	generalize in match stack'; -stack'
51	elim tl
52	[ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
53	elim globals in L';
54	[ normalize #E destruct
55	\| * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
56	#L cases (lookup_add_cases ??????? L)
57	[ * #E1 #E2 destruct
58	\| @IH
59	]
60	]
61	\| * #id2 #ty2 #tl2 #IH #stack' #vartypes'
62	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
63	#vartypes2 #stack2 #IH
64	whd in ⊢ (??%? → ?);
65	cases (orb ??)
66	[ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
67	[ * #E1 #E2 destruct //
68	\| #L'' lapply (IH ?? (refl ??) L'') /2/
69	]
70	\| #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
71	[ * #E1 #E2 destruct
72	\| #L'' lapply (IH ?? (refl ??) L'') /2/
73	]
74	]
75	]
76	\| -L #L #id' #n' #ty' #NE #L'
77	cases (lookup_add_cases ??????? L')
78	[ * #E1 #E2 destruct
79	%2 -IH -L'
80	generalize in match vartypes' in FOLD L; -vartypes'
81	generalize in match stack'; -stack'
82	elim tl
83	[ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
84	elim globals in L;
85	[ normalize #E destruct
86	\| * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
87	#L cases (lookup_add_cases ??????? L)
88	[ * #E1 #E2 destruct
89	\| @IH
90	]
91	]
92	\| * #id1 #ty1 #tl1 #IH #stack' #vartypes'
93	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
94	#vartypes2 #stack2 #IH
95	whd in ⊢ (??%? → ?);
96	cases (orb ??)
97	#E whd in E:(??%?); destruct
98	#L cases (lookup_add_cases ??????? L)
99	[ 1,3: * #E1 #E2 destruct //
100	\| 2,4: #L' lapply (IH ?? (refl ??) L') /2/
101	]
102	]
103	\| @(IH … (refl ??) L … NE)
104	]
105	\| -L #L #id' #n' #ty' #NE #L'
106	cases (lookup_add_cases ??????? L')
107	[ * #E1 #E2 destruct
108	\| @(IH … (refl ??) L … NE)
109	]
110	]
111	] qed.
112
113	(* And everything is in the stack frame. *)
114
115	lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
116	characterise_vars globals f = 〈vartypes, stacksize〉 →
117	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
118	n + sizeof ty ≤ stacksize.
119	#globals * #ret #args #vars #body whd in match (characterise_vars ??);
120	elim (args@vars)
121	[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
122	whd in FOLD:(??%?); destruct elim globals in L;
123	[ #E normalize in E; destruct
124	\| * * #id' #r' #ty' #tl' #IH
125	whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
126	[ * #E1 #E2 destruct
127	\| @IH
128	]
129	]
130	\| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
131	whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
132	#vartypes' #stackspace' #IH
133	whd in ⊢ (??(match % with [_⇒?])? → ?);
134	cases (orb ??) whd in ⊢ (??%? → ?);
135	#E destruct #L cases (lookup_add_cases ??????? L)
136	[ 1,3: * #E1 #E2 destruct //
137	\| 2,4: #L' lapply (IH … (refl ??) L') /2/
138	]
139	] qed.
140
141
142
143	(* Put knowledge that Globals are global into a more useful form than the
144	one used for the invariant. *)
145	(* XXX superfluous lemma ? Commenting it for now.
146	if not superfluous : move to toCminorCorrectnessExpr.ma, after
147	[characterise_vars_localid] *)
148	(*
149	lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
150	characterise_vars globals f = 〈vartypes, stacksize〉 →
151	∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
152	Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
153	¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
154	#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
155	cases (characterise_vars_src … CHAR id ?)
156	[ * #r' * #ty' >L
157	* #E1 destruct (E1) #EX
158	%
159	[ @EX
160	\| % #EX' cases (characterise_vars_localid … CHAR EX')
161	#ty' whd in ⊢ (% → ?); >L *
162	]
163	\| * #ty' whd in ⊢ (% → ?); >L *
164	\| whd >(opt_eq_from_res ???? L) % #E destruct
165	] qed. *)
166
167	(* Show how the global environments match up. *)
168
169	lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
170	map_partial_All A B P f l H = OK ? l' →
171	All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
172	#A #B #P #f #l
173	elim l
174	[ #H #l' #MAP normalize in MAP; destruct //
175	\| #h #t #IH * #p #H #l'
176	whd in ⊢ (??%? → ?);
177	lapply (refl ? (f h p)) whd in match (proj1 ???);
178	cases (f h p) in ⊢ (???% → %);
179	[ #b #E #MAP cases (bind_inversion ????? MAP)
180	#tl' * #MAP' #E' normalize in E'; destruct
181	% [ %{p} @E \| @IH [ @H \| @MAP' ] ]
182	\| #m #_ #X normalize in X; destruct
183	]
184	] qed.
185
186
187	definition clight_cminor_matching : clight_program → matching ≝
188	λp.
189	let tmpuniverse ≝ universe_for_program p in
190	let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
191	let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
192	let globals ≝ fun_globals @ var_globals in
193	mk_matching
194	?? (list init_data × type) (list init_data)
195	(λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
196	(λv,w. \fst v = w).
197
198	lemma clight_to_cminor_varnames : ∀p,p'.
199	clight_to_cminor p = OK ? p' →
200	prog_var_names … p = prog_var_names … p'.
201	* #vars #fns #main * #vars' #fns' #main'
202	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
203	whd in E:(??%%); destruct
204	-MAP normalize
205	elim vars
206	[ //
207	\| * * #id #r * #d #t #tl #IH normalize >IH //
208	] qed.
209
210	lemma clight_to_cminor_matches : ∀p,p'.
211	clight_to_cminor p = OK ? p' →
212	match_program (clight_cminor_matching p) p p'.
213	* #vars #fns #main * #vars' #fns' #main'
214	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
215	whd in E:(??%%); destruct
216	%
217	[ -MAP whd in match (m_V ?); whd in match (m_W ?);
218	elim vars
219	[ //
220	\| * * #id #r * #init #ty #tl #IH %
221	[ % //
222	\| @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
223	]
224	]
225	\| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
226	* #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
227	normalize in E; destruct
228	<(clight_to_cminor_varnames … TO)
229	% whd
230	% [2: % [2: @TRANSF \| skip ] \| skip ]
231	\| %
232	] qed.
233
234	(* A measure on Clight states that is decreasing along execution sequences *)
235
236	(* statements *)
237	let rec measure_Clight_statement (s : statement) : ℕ ≝
238	match s with
239	[ Sskip ⇒ 0
240	\| Ssequence s1 s2 ⇒
241	measure_Clight_statement s1 + measure_Clight_statement s2 + 1
242	\| Sifthenelse e s1 s2 =>
243	measure_Clight_statement s1 + measure_Clight_statement s2 + 1
244	\| Swhile e s =>
245	measure_Clight_statement s + 1
246	\| Sdowhile e s =>
247	measure_Clight_statement s + 1
248	\| Sfor s1 e s2 s3 =>
249	measure_Clight_statement s1 +
250	measure_Clight_statement s2 +
251	measure_Clight_statement s3 + 1
252	\| Sswitch e ls =>
253	measure_Clight_ls ls + 1
254	\| Slabel l s =>
255	measure_Clight_statement s + 1
256	\| Scost cl s =>
257	measure_Clight_statement s + 1
258	\| _ => 1
259	]
260	and measure_Clight_ls (ls : labeled_statements) : ℕ :=
261	match ls with
262	[ LSdefault s =>
263	measure_Clight_statement s
264	\| LScase sz i s ls =>
265	measure_Clight_statement s +
266	measure_Clight_ls ls
267	].
268
269	(* continuations *)
270	let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
271	match cont with
272	[ Kstop => 0
273	\| Kseq s k =>
274	measure_Clight_statement s +
275	measure_Clight_cont k + 1
276	\| Kwhile e s k =>
277	measure_Clight_statement s +
278	measure_Clight_cont k + 1
279	\| Kdowhile e s k =>
280	measure_Clight_statement s +
281	measure_Clight_cont k + 1
282	\| Kfor2 e s1 s2 k =>
283	measure_Clight_statement s1 +
284	measure_Clight_statement s2 +
285	measure_Clight_cont k + 1
286	\| Kfor3 e s1 s2 k =>
287	measure_Clight_statement s1 +
288	measure_Clight_statement s2 +
289	measure_Clight_cont k + 1
290	\| Kswitch k =>
291	measure_Clight_cont k + 1
292	\| Kcall retaddr f e k =>
293	measure_Clight_statement (fn_body f) +
294	measure_Clight_cont k + 1
295	].
296
297	(* Shamelessly copying Compcert. *)
298	definition measure_Clight : Clight_state → ℕ × ℕ ≝
299	λstate.
300	match state with
301	[ State f s k e m ⇒
302	〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
303	\| Callstate fb fd args k m ⇒ 〈0, 0〉
304	\| Returnstate res k m ⇒ 〈0, 0〉
305	\| Finalstate r ⇒ 〈0, 0〉
306	].
307
308	(* Stuff on lexicographic orders *)
309	definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
310	λA,Ord, x, y.
311	let 〈xa, xb〉 ≝ x in
312	let 〈ya, yb〉 ≝ y in
313	Ord xa ya ∨ (xa = ya ∧ Ord xb yb).
314
315	definition lex_lt ≝ lexicographic nat lt.
316
317
318	(* relate Clight continuations and Cminor ones. *)
319	inductive clight_cminor_cont_rel :
320	∀cl_ge, cm_ge.
321	∀INV: clight_cminor_inv cl_ge cm_ge. (* stuff on global variables and functions (matching between CL and CM) *)
322	∀cl_f: function. (* current Clight function *)
323	internal_function → (* current Cminor function *)
324	clight_cminor_data cl_f cl_ge cm_ge INV → (* data for the current stack frame in CL and CM *)
325	option typ → (* optional target type - uniform over a given function *)
326	cl_cont → (* CL cont *)
327	cm_cont → (* CM cont *)
328	Prop ≝
329	\| ClCm_cont_stop:
330	∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
331	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type Kstop Kend
332	\| ClCm_cont_seq:
333	∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
334	∀cl_s: statement.
335	∀cm_s: stmt.
336	∀cl_k': cl_cont.
337	∀cm_k': cm_cont.
338	∀stmt_univ, stmt_univ'.
339	∀lbl_univ, lbl_univ'.
340	∀lbls.
341	∀flag.
342	∀Htranslate_inv.
343	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» →
344	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
345	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
346	\| ClCm_cont_while:
347	(* Inductive family parameters *)
348	∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
349
350	(* sub-continuations *)
351	∀cl_k': cl_cont.
352	∀cm_k': cm_cont.
353
354	(* elements of the source while statement *)
355	∀sz,sg.
356	∀cl_cond_desc.
357	∀cl_body.
358
359	(* elements of the converted while statement *)
360	∀cm_cond: CMexpr (ASTint sz sg).
361	∀cm_body.
362	∀entry,exit: identifier Label.
363
364	(* universes used to generate fresh labels and variables *)
365	∀stmt_univ, stmt_univ'.
366	∀lbl_univ, lbl_univ', lbl_univ''.
367	∀lbls: lenv.
368	∀Htranslate_inv.
369
370	(* relate CL and CM expressions *)
371	∀Hexpr_vars.
372	translate_expr (alloc_type … frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
373
374	(* Parameters and results to find_label_always *)
375	∀sInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f).
376	∀Hinv.
377
378	(* Specify how the labels for the while-replacing gotos are produced *)
379	mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
380	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» →
381	find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env … frame_data) sInv I =
382	«〈St_label entry
383	(St_seq
384	(St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
385	(St_label exit St_skip)), cm_k'〉, Hinv» →
386	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
387	clight_cminor_cont_rel cl_ge cm_ge 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')).
388
389	(* Definition of the simulation relation on states. The orders of the parameters is dictated by
390	* the necessity of performing an inversion on the continuation sim relation without having to
391	* play the usual game of lapplying all previous dependent arguments. *)
392	inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge → Clight_state → Cminor_state → Prop ≝
393	\| CMR_normal :
394	∀cl_ge, cm_ge.
395	(* Relates globals to globals and functions to functions. *)
396	∀INV: clight_cminor_inv cl_ge cm_ge.
397
398	(* ---- Statements ---- *)
399	∀cl_s: statement. (* Clight statement *)
400	∀cm_s: stmt. (* Cminor statement *)
401
402	(* ---- Continuations ---- *)
403	∀cl_k: cl_cont. (* Clight continuation *)
404	∀cm_k: cm_cont. (* Cminor continuation *)
405	∀cm_st: stack. (* Cminor stack *)
406
407	∀cl_f: function. (* Clight enclosing function *)
408	∀cm_f: internal_function. (* enclosing function *)
409	∀frame_data: clight_cminor_data cl_f ?? INV.
410	∀rettyp. (* return type of the function *)
411
412	(* ---- Relate Clight continuation to Cminor continuation ---- *)
413	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
414
415	(* ---- Other Cminor variables ---- *)
416	∀fInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f). (* Cminor invariants *)
417	∀sInv: stmt_inv cm_f (cm_env … frame_data) cm_s.
418	∀kInv: cont_inv cm_f (cm_env … frame_data) cm_k.
419
420	(* ---- Relate return type variable to actual return type ---- *)
421	rettyp = opttyp_of_type (fn_return cl_f) →
422
423	(* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
424
425	(* ---- relate Clight and Cminor functions ---- *)
426	∀func_univ: universe SymbolTag.
427	∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
428	∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
429	translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
430
431	(* ---- relate Clight and Cminor statements ---- *)
432	∀stmt_univ,stmt_univ': tmpgen (alloc_type … frame_data).
433	∀lbl_univ,lbl_univ': labgen.
434	∀lbls: lenv.
435	∀flag: convert_flag.
436	∀Htranslate_inv.
437	translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
438
439	clight_cminor_rel cl_ge cm_ge INV
440	(ClState cl_f cl_s cl_k (cl_env … frame_data) (cl_m … frame_data))
441	(CmState cm_f cm_s (cm_env … frame_data) fInv sInv (cm_m … frame_data) (stackptr … frame_data) cm_k kInv cm_st)
442
443	\| CMR_return :
444	∀cl_ge, cm_ge, cl_f.
445	∀INV: clight_cminor_inv cl_ge cm_ge.
446	∀frame_data: clight_cminor_data cl_f ?? INV.
447	∀cl_mem, cm_mem.
448	cl_mem = cl_m … frame_data →
449	cm_mem = cm_m … frame_data →
450	∀cm_st: stack. (* Cminor stack *)
451	clight_cminor_rel cl_ge cm_ge INV
452	(ClReturnstate Vundef Kstop cl_mem)
453	(CmReturnstate (None val) cm_mem cm_st)
454
455	\| CMR_call :
456	∀cl_ge, cm_ge, cl_f, cm_f.
457	∀INV: clight_cminor_inv cl_ge cm_ge.
458	∀frame_data: clight_cminor_data cl_f cl_ge cm_ge INV.
459	∀u: universe SymbolTag.
460	∀cl_fundef, cm_fundef.
461	∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
462	∀Hfundef_fresh: fd_fresh_for_univ cl_fundef u.
463	∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
464	∀cl_k, cm_k.
465	clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
466	∀fblock.
467	match cl_fundef with
468	[ CL_Internal cl_function ⇒
469	find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
470	find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
471	translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef
472	\| CL_External name argtypes rettype ⇒
473	True
474	] →
475	∀fptr_block.
476	∀sInv, fInv, kInv.
477	∀cl_args_values, cm_args_values.
478	(* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
479	∀cm_stack.
480	clight_cminor_rel cl_ge cm_ge INV
481	(ClCallstate (Vptr (mk_pointer fptr_block zero_offset))
482	cl_fundef cl_args_values
483	(Kcall (None (block×offset×type)) cl_f (cl_env ???? frame_data) cl_k)
484	(cl_m ???? frame_data))
485	(CmCallstate (Vptr (mk_pointer fptr_block zero_offset)) cm_fundef
486	cm_args_values (cm_m ???? frame_data)
487	(Scall (None (ident×typ)) cm_f (stackptr ???? frame_data) (cm_env ???? frame_data) sInv fInv cm_k kInv cm_stack)).
488
489	definition clight_normal : Clight_state → bool ≝
490	λs. match Clight_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
491
492	definition cminor_normal : Cminor_state → bool ≝
493	λs. match Cminor_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
494
495	definition cl_pre : preclassified_system ≝
496	mk_preclassified_system
497	clight_fullexec
498	(λg. Clight_labelled)
499	(λg. Clight_classify)
500	(λf,g,s,H. 0). (* XXX TODO *)
501
502	definition cm_pre : preclassified_system ≝
503	mk_preclassified_system
504	Cminor_fullexec
505	(λg. Cminor_labelled)
506	(λg. Cminor_classify)
507	(λf,g,s,H. 0). (* XXX TODO *)
508
509	(* Auxilliary lemmas. *)
510
511	lemma invert_assert :
512	∀b. ∀P. assert b P → b = true ∧ P.
513	* #P whd in ⊢ (% → ?); #H
514	[ @conj try @refl @H
515	\| @False_ind @H ]
516	qed.
517
518	lemma res_to_io :
519	∀A,B:Type[0]. ∀C.
520	∀x: res A. ∀y.
521	match x with
522	[ OK v ⇒ Value B C ? v
523	\| Error m ⇒ Wrong … m ] = return y →
524	x = OK ? y.
525	#A #B #C *
526	[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
527	\| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
528	qed.
529
530	lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
531	#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
532
533	(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
534	lemma pair_eq_split :
535	∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
536	〈a1,b1〉 = 〈a2, b2〉 →
537	a1 = a2 ∧ b1 = b2.
538	#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
539	qed.
540
541	lemma ok_eq_ok_destruct :
542	∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
543	#H1 #H2 #H3 #H4 destruct @refl qed.
544
545	lemma sigma_eq_destruct : ∀A:Type[0]. ∀a,b:A. ∀P: A → Prop. ∀Ha: P a. ∀Hb: P b. «a, Ha» = «b,Hb» → a = b ∧ Ha ≃ Hb.
546	#A #a #b #P #Ha #Hb #Heq destruct (Heq)
547	@conj try %
548	qed.
549
550	(* inverting find_funct and find_funct_ptr *)
551	lemma find_funct_inversion :
552	∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
553	find_funct F ge v = Some ? res →
554	(∃ptr. v = Vptr ptr ∧
555	(poff ptr) = zero_offset ∧
556	block_region (pblock ptr) = Code ∧
557	(∃p. block_id (pblock ptr) = neg p ∧
558	lookup_opt … p (functions … ge) = Some ? res)).
559	#F #ge #v #res
560	cases v
561	[ \| #sz #i \| \| #ptr ]
562	whd in ⊢ ((??%?) → ?);
563	#Heq destruct (Heq)
564	%{ptr} @conj try @conj try @conj try @refl
565	lapply Heq -Heq
566	@(eq_offset_elim … (poff ptr) zero_offset) //
567	normalize nodelta
568	[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
569	#Heq destruct (Heq)
570	whd in ⊢ ((??%?) → ?);
571	cases ptr #blo #off cases (block_region blo) normalize nodelta
572	[ 1,3: #Habsurd destruct (Habsurd) ]
573	[ // ]
574	cases (block_id blo) normalize nodelta
575	[ #Habsurd destruct (Habsurd) \| #p #Habsurd destruct (Habsurd) ]
576	#p #Hlookup %{p} @conj try @refl assumption
577	qed.
578
579	(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
580	lemma translate_dest_id_inversion :
581	∀var_types, e, var_id, ty,H.
582	translate_dest var_types e = return IdDest var_types var_id ty H →
583	e = Expr (Evar var_id) (typeof e).
584	@cthulhu
585	(*
586	#vars #e #var_id #ty #H
587	cases e #ed #ty'
588	cases ed
589	[ #sz #i \| #id \| #e1 \| #e1 \| #op #e1 \|#op #e1 #e2 \| #cast_ty #e1
590	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
591	whd in ⊢ ((??%%) → ?);
592	#Heq
593	[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
594	\| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
595	#_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
596	lapply Heq -Heq
597	change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
598	cases (bind2_eq_inversion ?????? Heq)
599	#alloctype
600	(* * #alloctype ) #typ' *
601	cases alloctype
602	[ #r \| #n \| ] normalize nodelta #Hlookup'
603	[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
604	whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
605	@refl*)
606	qed.
607
608
609	(* Note: duplicate in switchRemoval.ma *)
610	lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
611
612	lemma breakup_dependent_match_on_pairs :
613	∀A,B,C: Type[0].
614	∀term: A × B.
615	∀F: ∀x,y. 〈x, y〉 = term → C.
616	∀z:C.
617	match term
618	return λx.x = term → ? with
619	[ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
620	∃xa,xb,H. term = 〈xa, xb〉 ∧
621	F xa xb H = z.
622	#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
623	// qed.
624
625
626	lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
627	translate_expr_sigma vars cl_expr = OK ? cm_expr →
628	dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
629	#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
630	whd in ⊢ ((??%?) → ?); #H
631	cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
632	#Htranslate_expr
633	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
634	qed.
635
636	lemma translate_exprlist_sigma_welltyped :
637	∀vars, cl_exprs, cm_exprs.
638	mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
639	All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
640	#vars #cl_exprs
641	elim cl_exprs
642	[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
643	\| #hd #tl #Hind * #cm_exprs #Hall #H
644	cases (bind_inversion ????? H) -H
645	* * #cm_typ #cm_expr normalize nodelta
646	#Hexpr_vars_cm * #Htranslate_hd
647	lapply (translate_expr_sigma_welltyped … Htranslate_hd)
648	#Heq_cm_typ #H
649	cases (bind_inversion ????? H) -H
650	#cm_tail lapply (Hind cm_tail) cases cm_tail
651	#cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
652	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
653	[ @Heq_cm_typ
654	\| @Hind assumption ]
655	] qed.
656
657	lemma translate_dest_MemDest_simulation :
658	∀f.
659	∀cl_ge : genv_t clight_fundef.
660	∀cm_ge : genv_t (fundef internal_function).
661	∀INV : clight_cminor_inv cl_ge cm_ge.
662	∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
663	∀cl_expr. ∀cm_expr.
664	∀cl_block, cl_offset, trace.
665	∀Hyp_present.
666	translate_dest (alloc_type … frame_data) cl_expr = OK ? (MemDest ? cm_expr) →
667	exec_lvalue cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
668	∃cm_val. eval_expr cm_ge ASTptr cm_expr (cm_env … frame_data) Hyp_present (stackptr … frame_data) (cm_m … frame_data) = OK ? 〈trace, cm_val〉 ∧
669	value_eq (Em … frame_data) (Vptr (mk_pointer cl_block cl_offset)) cm_val.
670	#f #cl_ge #cm_ge #INV #frame_data #cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
671	whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
672	cases cl_desc normalize nodelta
673	[ #sz #i \| #id \| #e1 \| #e1 \| #op #e1 \|#op #e1 #e2 \| #cast_ty #e1
674	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
675	#Htranslate
676	[ 2:
677	\| : cases (bind_inversion ????? Htranslate) -Htranslate #cm_expr' #Hexpr_vars' *
678	#Htranslate_addr
679	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
680	cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #_ #Hsim
681	@(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
682	cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
683	[ #r \| #n \| ]
684	* #cl_type * #Heq_lookup normalize nodelta
685	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
686	whd in ⊢ ((??%?) → ?);
687	@(match lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id
688	return λx. (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id = x) → ?
689	with
690	[ None ⇒ ?
691	\| Some loc ⇒ ?
692	] (refl ? (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id ))) normalize nodelta
693	#Hlookup_eq
694	[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
695	[ 2: %{(Vptr (mk_pointer (stackptr f cl_ge cm_ge INV frame_data)
696	(shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
697	@conj try @refl
698	lapply (matching … frame_data id)
699	>Hlookup_eq normalize nodelta
700	>(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
701	#Hembed %4 whd in ⊢ (??%?); >Hembed @refl
702	\| 1: whd in match (eval_constant ????);
703	lapply (matching … frame_data id)
704	>Hlookup_eq normalize nodelta
705	>(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
706	@False_ind
707	]
708	\| 1,3: #Hfind_symbol
709	cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
710	whd in ⊢ ((??%%) → ?); #Hfind_symbol
711	lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
712	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
713	whd in match (eval_expr ???????);
714	whd in match (eval_constant ????);
715	lapply (matching … frame_data id)
716	[ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
717	#Hembed
718	<(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
719	%{(Vptr
720	(mk_pointer cl_block
721	(shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
722	@conj try @refl
723	%4 whd in ⊢ (??%?); >Hembed try @refl
724	\| (* A stack variable is not in the local environment but in the global one. *)
725	(* we have a contradiction somewhere in the context *)
726	(* TODO *)
727	@cthulhu
728	]
729	] qed.
730
731	(* lift simulation result to eval_exprlist *)
732	lemma eval_exprlist_simulation :
733	∀f.
734	∀cl_ge : genv_t clight_fundef.
735	∀cm_ge : genv_t (fundef internal_function).
736	∀INV : clight_cminor_inv cl_ge cm_ge.
737	∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
738	∀cl_exprs,cm_exprs.
739	∀cl_results,trace.
740	exec_exprlist cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_exprs = OK ? 〈cl_results, trace〉 →
741	mmap_sigma ??? (translate_expr_sigma (alloc_type … frame_data)) cl_exprs = OK ? cm_exprs →
742	∀H:All ? (λx:𝚺t:typ.expr t.
743	match x with
744	[ mk_DPair ty e ⇒
745	(expr_vars ty e
746	(λid:ident.λty:typ.present SymbolTag val (cm_env … frame_data) id)) ]) cm_exprs.
747	∃cm_results.
748	trace_map_inv … (λe. match e return λe.
749	match e with
750	[ mk_DPair _ _ ⇒ ? ] → ?
751	with
752	[ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e (cm_env … frame_data) p (stackptr … frame_data) (cm_m … frame_data) ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
753	All2 ?? (λcl_val, cm_val. value_eq (Em … frame_data) cl_val cm_val) cl_results cm_results.
754	#f #cl_ge #cm_ge #INV #frame_data #cl_exprs
755	elim cl_exprs
756	[ #cm_exprs #cl_results #trace
757	whd in ⊢ ((??%?) → ?);
758	#Heq destruct (Heq)
759	whd in ⊢ ((??%?) → ?);
760	#Heq destruct (Heq) #H %{[]}
761	@conj try @refl try @I
762	\| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
763	#Heq cases (bind_inversion ????? Heq) -Heq
764	* #hd_val #hd_trace * #Hexec_expr_cl
765	#Heq cases (bind_inversion ????? Heq) -Heq
766	* #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
767	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
768	#Htranslate
769	lapply (translate_exprlist_sigma_welltyped … Htranslate)
770	#Htype_eq_all #Hall
771	cases (bind_inversion ????? Htranslate) -Htranslate
772	* * #cmtype #cmexpr normalize nodelta
773	#Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
774	cases (bind_inversion ????? Htranslate) -Htranslate
775	* #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
776	normalize nodelta
777	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
778	cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
779	lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
780	[ assumption ] -Hind #Hind
781	lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
782	* #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
783	cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #Hsim #_
784	cases (bind_inversion ????? Htranslate_expr_sigma)
785	* #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
786	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
787	lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
788	[ @(proj1 ?? Hall) ]
789	* #cm_val_hd * #Heval_expr_cm #Hvalue_eq
790	%{(cm_val_hd :: cm_results_tl)} @conj
791	[ 2: @conj try assumption
792	\| 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
793	normalize nodelta >Hcm_exec_tl @refl
794	]
795	] qed.
796
797	(* Conjectured simulation results
798
799	We split these based on the start state:
800
801	1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
802	normal steps in Cminor;
803	2. call and return steps are simulated by a call/return step plus [m] normal
804	steps (to copy stack allocated parameters / results); and
805	3. lone cost label steps are simulates by a lone cost label step
806
807	These should allow us to maintain enough structure to identify the Cminor
808	subtrace corresponding to a measurable Clight subtrace.
809	*)
810
811	lemma clight_cminor_normal :
812	∀g1,g2.
813	∀INV:clight_cminor_inv g1 g2.
814	∀s1,s1'.
815	clight_cminor_rel g1 g2 INV s1 s1' →
816	clight_normal s1 →
817	¬ pcs_labelled cl_pre g1 s1 →
818	∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →
819	∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
820	tr = tr' ∧
821	clight_cminor_rel g1 g2 INV s2 s2' ∧
822	(m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
823	).
824	#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
825	inversion Hstate_rel
826	#cl_ge #cm_ge #INV' #cl_s
827	(* case analysis on Clight statement *)
828	cases cl_s
829	[ 1: \| 2: #lhs #rhs \| 3: #retv #func #args \| 4: #stm1 #stm2 \| 5: #cond #iftrue #iffalse \| 6: #cond #body
830	\| 7: #cond #body \| 8: #init #cond #step #body \| 9,10: \| 11: #retval \| 12: #cond #switchcases \| 13: #lab #body
831	\| 14: #lab \| 15: #cost #body ]
832	[ 3: (* Call *)
833	#cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
834	(* introduce everything *)
835	#fInv #sInv #kInv
836	#Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
837	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
838	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
839	#Hreturn_ok #Hlabel_wf
840	(* generalize away ugly proof *)
841	generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
842	#Htranslate
843	@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
844	destruct (HA HB)
845	@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
846	destruct (HC HD HE) #_
847	(* back to unfolding Clight execution *)
848	cases (bind_inversion ????? Htranslate) -Htranslate *
849	#ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
850	cases (bind_inversion ????? Htranslate) -Htranslate *
851	#ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
852	cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
853	-Htyp_should_eq_ef #Htyp_equality_ef
854	#Heq_ef_ef' #Htranslate
855	cases (bind_inversion ????? Htranslate) -Htranslate *
856	#args #Hall_variables_from_args_local *
857	whd in ⊢ ((???%) → ?); #Hargs_spec
858	cases retv normalize nodelta
859	[ 2: (* return something *)
860	#lhs #Hdest
861	cases (bind_inversion ????? Hdest) -Hdest #dest *
862	inversion dest normalize nodelta
863	[ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
864	#Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
865	(* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
866	lapply (translate_dest_id_inversion … Htranslate_dest) #Hlhs_eq
867	\| * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
868	lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
869	* #ret_var * #new_gensym * #Heq_alloc_tmp * #Halloc_tmp #Hgensym
870	lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
871	* #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #Halloc_tmp'
872	generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
873	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
874	]
875	\| 1: (* return void *)
876	generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
877	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
878	#s2 #tr #Htranslate
879	cases (bindIO_inversion ??????? Htranslate) -Htranslate *
880	#func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
881	whd in ⊢ ((???%) → ?); #Htranslate
882	cases (bindIO_inversion ??????? Htranslate) -Htranslate *
883	#args_values #args_trace * #Hexec_arglist #Htranslate
884	cases (bindIO_inversion ??????? Htranslate) -Htranslate
885	#cl_fundef * #Hfind_funct
886	lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
887	cases (find_funct_inversion ???? Hfind_funct)
888	#func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
889	#Hpoff_eq_zero #Hregion_is_code
890	* #block_id * #Hblock_id_neg #Hlookup
891	#Htranslate
892	cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
893	#Hassert_type_eq
894	[ 1,2: #Htranslate
895	cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
896	#lblock #loffset #ltrace *
897	#Hexec_lvalue
898	[ 1: (* empty trace ) @cthulhu ( TODO wip *)
899	\| 2: @cthulhu (* TODO wip *)
900	]
901	\| 3: @cthulhu ]
902	(* TODO wip *)
903	(*
904	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
905	[ 1: >Hlhs_eq in Hexec_lvalue; #Hexec_lvalue %{1}
906	\| 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
907	%{2} whd whd in ⊢ (??%?); normalize nodelta
908	whd in match (eval_expr ???????);
909	whd in match (m_bind ?????);
910	lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
911	-Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
912
913	\| 3:
914	]
915	(* execute Cminor part *)
916	[ %{1} \| %{2} \| %{1} ]
917	whd whd in ⊢ (??%?); normalize nodelta
918	[ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
919	\| 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
920	\| 3: generalize in match (proj2 True ??); ]
921	#Hexpr_vars_present_ef'
922	cases (eval_expr_sim … frame_data) #Hsim_expr #_
923	cut (expr_vars (typ_of_type (typeof func)) ef
924	(λid:ident.λty:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id))
925	[ 1,3,5: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
926	#ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
927	@Hexpr_vars_present_ef' ]
928	#Hexpr_vars_present_ef
929	(* use simulation lemma on expressions for function *)
930	lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
931	-Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
932	cut (eval_expr cm_ge ASTptr ef'
933	(cm_env cl_f cl_ge cm_ge INV' frame_data) Hexpr_vars_present_ef'
934	(stackptr cl_f cl_ge cm_ge INV' frame_data)
935	(cm_m cl_f cl_ge cm_ge INV' frame_data)
936	=OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
937	[ 1,3,5:
938	lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
939	lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
940	<Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
941	@(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
942	-Heval_func #Heval_func >Heval_func
943	whd in match (m_bind ?????);
944	lapply (trans_fn … INV' … Hfind_funct)
945	* #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
946	#Htranslate_fundef #Hfind_funct_cm
947	lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
948	whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
949	#cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
950	whd in ⊢ ((??%?) → ?); >(Em_fn_id … frame_data … cm_block Hregion_is_code)
951	normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
952	#Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) >addition_n_0
953	>Hfind_funct_cm
954	whd in match (opt_to_res ???); normalize nodelta
955	cut (All (𝚺t:typ.CMexpr t)
956	(λx:𝚺t:typ.expr t.(
957	match x with
958	[ mk_DPair ty e ⇒
959	expr_vars ty e
960	(λid:ident
961	.λty0:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)])) args)
962	[ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
963	\| 3: cases sInv * * * * * * * normalize nodelta * #_ #_ #Hall #_ #_ #_ @Hall
964	\| 5: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
965	#Hall
966	cases (eval_exprlist_simulation … frame_data ???? Hexec_arglist Hargs_spec Hall)
967	#cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
968	whd in match (m_bind ?????); normalize nodelta whd (* TODO here bug in toCminor to be fixed before going on *) @conj
969	[ 2,4,6: #Habsurd destruct (Habsurd) ]
970	@conj try @refl
971	generalize in match (proj1 True (expr_vars ???) (proj1 ???));
972	* @(CMR_call … tmp_u) try assumption normalize nodelta
973	(* a dependency somewhere prevents case analysis *)
974	lapply Hfind_funct lapply Hfind_funct_cm lapply Htranslate_fundef lapply Hfundef_fresh_for_tmp_u
975	cases cl_fundef
976	[ 2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 @I
977	\| 1: #H9 #H10 #H11 #H12 #H13 @conj try @conj try // ]
978	\| (* return something *)
979	#lhs #Hdest
980	cases (bind_inversion ????? Hdest) -Hdest #dest *
981	inversion dest normalize nodelta
982	[ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
983	#Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
984	generalize in match (conj ???);
985	]
986
987
988	whd in match (proj1 ???); whd in match (proj2 ???);
989
990
991	[ 2: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
992
993	>Hfind_funct_cm
994	(* case split away the invariants *)
995	cases sInv * * normalize nodelta * * #Hexpr_vars_ef' #Hall_args_present
996	whd in ⊢ (% → ?); * * normalize nodelta * #Heval_expr #Hvalue_eq
997	>Heval_expr
998	*
999
1000	[ 1: (* Skip *)
1001	#cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
1002	(* case analysis on continuation *)
1003	inversion Hcont_rel
1004	[ (* Kstop continuation *)
1005	(* simplifying the goal using outcome of the inversion *)
1006	#kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
1007	@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1008	destruct (HA HB)
1009	@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1010	destruct (HC HD HE)
1011	@(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
1012	destruct (HF HG HH HI) #_
1013	(* introduce everything *)
1014	#fInv #sInv #kInv
1015	#Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1016	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1017	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1018	#Hreturn_ok #Hlabel_wf
1019	(* reduce statement translation function *)
1020	whd in ⊢ ((??%?) → ?);
1021	#Heq_translate
1022	(* In this simple case, trivial translation *)
1023	destruct (Heq_translate)
1024	@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1025	destruct (HA HB)
1026	@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1027	destruct (HC HD HE) #_
1028	(* unfold the clight execution *)
1029	#s2 #tr whd in ⊢ ((??%?) → ?);
1030	inversion (fn_return kcl_f) normalize nodelta
1031	normalize nodelta
1032	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1033	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1034	#Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1035	%{1} whd @conj try @conj try @refl
1036	[ 2: #Habsurd destruct (Habsurd) ]
1037	%2{kcl_f}
1038	[ %{ (alloc_type … kframe_data)
1039	(stacksize … kframe_data)
1040	(alloc_hyp … kframe_data)
1041	(cl_env … kframe_data)
1042	(cm_env … kframe_data)
1043	(cl_env_hyp … kframe_data)
1044	(free_list (cl_m … kframe_data) (blocks_of_env (cl_env … kframe_data)))
1045	(free (cm_m … kframe_data) (stackptr … kframe_data))
1046	(Em … kframe_data)
1047	? (* injection *)
1048	(stackptr … kframe_data)
1049	? (* matching *)}
1050	[ @(freelist_memory_inj_m1_m2 … (injection … kframe_data) (blocks_of_env (cl_env … kframe_data)) (stackptr … kframe_data))
1051	[ 2,3: @refl
1052	\|
1053
1054	@cthulhu
1055	\| (* KSeq continuation *)
1056	#gcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
1057	#kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
1058	* * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
1059	#kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
1060	@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1061	destruct (HA HB)
1062	@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1063	destruct (HC HD HE)
1064	@(jmeq_absorb ?????) #HF
1065
1066	#Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k #_
1067	(* get rid of jmeqs and destruct *)
1068	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1069	lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
1070	destruct (Heq_INV Heq_cl_f)
1071	lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
1072	lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
1073	lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
1074	lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
1075	lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
1076	destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)
1077	#fInv #sInv #kInv #Hktarget_type
1078	#func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1079	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1080	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1081	#Hreturn_ok #Hlabel_wf
1082	(* reduce translation function and eliminate result *)
1083	(* In this simple case, trivial translation *)
1084	whd in ⊢ ((??%?) → ?); #Heq_translate
1085	destruct (Heq_translate)
1086	#Heq_INV' #Heq_s1 #Heq_s1'
1087	lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
1088	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1089	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
1090	(* unfold the clight execution *)
1091	%{0}
1092	whd in ⊢ (% → ?); #Hassert
1093	cases (invert_assert ?? Hassert) -Hassert #Hclight_class
1094	cases (andb_inversion … Hclight_class) -Hclight_class
1095	#_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
1096	%{0} whd in ⊢ %; @conj try @refl
1097	(* close simulation *)
1098	%1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
1099	Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
1100	[ 3: @kHeq_translate \| assumption ]
1101	\| (* Kwhile continuation *)
1102	#kINV #kcl_f #kcm_f #kframe_data #ktarget_type
1103	#kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
1104	#kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
1105	#klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
1106	* * * * #kHentry_declared * * * *
1107	* * * #kHcond_vars_declared * * * *
1108	* * * #kHbody_inv * * *
1109	whd in ⊢ (% → ?); #kHentry_declared'
1110	* * * * * * * * *
1111	whd in ⊢ (% → ?); #kHexit_declared *
1112	* * * *
1113	#kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
1114	#Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
1115	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1116	lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
1117	destruct (Heq_INV Heq_cl_f)
1118	lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
1119	lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
1120	lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
1121	lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
1122	lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
1123	destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
1124	(* introduce state relation contents *)
1125	#fInv #sInv * whd in ⊢ (% → ?); * *
1126	whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
1127	#Heq_rettyp
1128	#func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1129	#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1130	#flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1131	#Hreturn_ok #Hlabel_wf
1132	(* reduce translation function and eliminate result *)
1133	(* In this simple case, trivial translation *)
1134	whd in ⊢ ((??%?) → ?); #Heq_translate
1135	destruct (Heq_translate)
1136	#Heq_INV' #Heq_s1 #Heq_s1'
1137	lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
1138	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1139	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
1140	(* unfold the clight execution *)
1141	%{1} whd in ⊢ (% → ?); #Hawait
1142	cases (await_value_bind_inv … Hawait) -Hawait
1143	* #cl_val #cl_trace * #Hexec_cond #Hawait
1144	cases (await_value_bind_inv … Hawait) -Hawait
1145	#cond_outcome * #Hcond_outcome
1146	cases (eval_expr_sim … kframe_data) #Hsim_expr #_
1147	(* use simulation lemma on expressions *)
1148	lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
1149	whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
1150	#Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
1151	* [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
1152	* [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
1153	* #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
1154	normalize nodelta #Hi_eq
1155	* #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
1156	cases (invert_assert … Hassert) -Hassert #Handb
1157	cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
1158	whd in ⊢ (% → ?); #Heq destruct (Heq)
1159	[ %{5} whd whd in ⊢ (??%?); normalize nodelta
1160	>kHfind_label -kHfind_label normalize nodelta
1161	whd in match (proj1 ???);
1162	whd in match (proj2 ???);
1163	whd whd in ⊢ (??%?); normalize nodelta
1164	>Hexec_cond_cm normalize nodelta
1165	whd in match (m_bind ?????);
1166	>(value_eq_int_inversion … Hvalue_eq)
1167	whd in match (eval_bool_of_val ?); normalize nodelta
1168	<Hi_eq normalize nodelta
1169	whd @conj [ normalize >append_nil try @refl ]
1170	whd in match (proj1 ???);
1171	whd in match (proj2 ???);
1172	whd whd in ⊢ (??%?); normalize nodelta
1173	%{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
1174	??????? kHeq_translate}
1175	\| %{6} whd whd in ⊢ (??%?); normalize nodelta
1176	>kHfind_label -kHfind_label normalize nodelta
1177	whd in match (proj1 ???);
1178	whd in match (proj2 ???);
1179	whd whd in ⊢ (??%?); normalize nodelta
1180	>Hexec_cond_cm normalize nodelta
1181	whd in match (m_bind ?????);
1182	>(value_eq_int_inversion … Hvalue_eq)
1183	whd in match (eval_bool_of_val ?); normalize nodelta
1184	<Hi_eq normalize nodelta
1185	whd @conj [ normalize >append_nil >append_nil try @refl ]
1186	whd in match (proj1 ???);
1187	whd in match (proj2 ???);
1188	whd whd in ⊢ (??%?); normalize nodelta
1189	%{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
1190	try assumption
1191	[ @conj try @conj try @conj try @conj //
1192	\| @refl ]
1193	]
1194	(\| TODO: other continuations )
1195	]
1196	\| 2: (* Assign *)
1197	#cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
1198	#fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
1199	#Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
1200	* * * * #Hstmt_inv_cm #Huseless_hypothesis
1201	#Htmps_preserved #Hreturn_ok #Hlabel_wf
1202	(* case-split on lhs in order to reduce lvalue production in Cminor *)
1203	cases lhs #lhs_ed #lhs_ty
1204	cases lhs_ed
1205	(* intro expr contents *)
1206	[ #sz #i \| #var_id \| #e1 \| #e1 \| #op #e1 \|#op #e1 #e2 \| #cast_ty #e1
1207	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
1208	[ 2: #Htranslate_statement
1209	cases (bind_inversion ????? Htranslate_statement)
1210	* #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
1211	cases (bind_inversion ????? Htranslate_statement')
1212	#lhs_dest * #Htranslate_lhs
1213	cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
1214	#alloctype * #type_of_var * #Hlookup_var_success
1215	cases alloctype in Hlookup_var_success;
1216	normalize nodelta
1217	[ 1: (* Global *) #r
1218	#Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
1219	destruct (Hlhs_dest_eq) normalize nodelta
1220	whd in match (proj1 ???); whd in match (proj2 ???);
1221	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1222	#Heq_INV #Heq_s1 #Heq_s1'
1223	lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1224	lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1225	lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
1226	destruct (Heq_INV Heq_s1 Heq_s1') #_
1227	%{1} whd in ⊢ (% → ?); #Hawait
1228	cases (await_value_bind_inv … Hawait) -Hawait
1229	* * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
1230	#Hexec_lvalue
1231	lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
1232	#Hawait
1233	cases (await_value_bind_inv … Hawait) -Hawait
1234	* #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
1235	cases (await_value_bind_inv … Hawait) -Hawait
1236	#mem_after_store * #Hstore_value #Hawait
1237	lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
1238	-Htranslate_statement' -Htranslate_statement
1239	cases (invert_assert … Hawait) -Hawait #Handb
1240	cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait
1241	(* TODO: use the memory injection to handle the store,
1242	use INV contents to match up CL global with CM one.
1243	Note to self: globals should be exactly matched in CL and CM,
1244	maybe memory_injection is not useful in this particular case,
1245	only in Stack and Local cases.
1246	* *)
1247	@cthulhu
1248	\| 2: (* Stack *) #n @cthulhu
1249	\| 3: (* Local *) @cthulhu
1250	]
1251	\| : ( memdest ) @cthulhu ] )
1252	\| *: @cthulhu
1253	] qed.
1254
1255	(* TODO: adapt the following to the new goal shape. *)
1256	axiom clight_cminor_call_return :
1257	∀INV:clight_cminor_inv.
1258	∀s1,s1',s2,tr.
1259	clight_cminor_rel INV s1 s1' →
1260	match Clight_classify s1 with [ cl_call ⇒ true \| cl_return ⇒ true \| _ ⇒ false ] →
1261	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1262	∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1263	tr = tr' ∧
1264	clight_cminor_rel INV s2 s2'
1265	).
1266
1267	axiom clight_cminor_cost :
1268	∀INV:clight_cminor_inv.
1269	∀s1,s1',s2,tr.
1270	clight_cminor_rel INV s1 s1' →
1271	Clight_labelled s1 →
1272	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1273	after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
1274	tr = tr' ∧
1275	clight_cminor_rel INV s2 s2'
1276	).
1277
1278	axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
1279	clight_to_cminor cl_program = OK ? cm_program →
1280	make_initial_state ?? clight_fullexec cl_program = OK ? s →
1281	make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
1282	∃INV. clight_cminor_rel INV s s'.

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

Download in other formats:

Original Format