Context Navigation

toCminorCorrectness.ma @ 2562

Last change on this file since 2562 was 2554, checked in by garnier, 8 years ago

Proof of expression translation correctness "mostly" done for CL to CM. Some inconsistencies found in bit width for constants
regarding boolean operators need to be fixed (either by modifying CL semantics of by making CM code generation inefficient).
An inconsistency between clight and cminor expression evaluation was found for cost labels (placed before and after trace) - not
fixed yet, for fear of breaking proofs. One or two small lemmas missing, and most importantly, binary operators not done yet.

File size: 71.9 KB

Line
1	include "Clight/toCminor.ma".
2
3	(* When we characterise the local Clight variables, those that are stack
4	allocated are given disjoint regions of the stack. *)
5
6	lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7	characterise_vars globals f = 〈vartypes, stacksize〉 →
8	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9	∀id',n',ty'. id ≠ id' →
10	lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11	n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12	#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13	whd in ⊢ (??%? → ?);
14	generalize in match vartypes; -vartypes
15	generalize in match stacksize; -stacksize
16	elim (args@vars)
17	[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18	elim globals in L;
19	[ normalize #L destruct
20	\| * * #id' #r #ty' #tl #IH
21	whd in match (foldr ?????);
22	#L cases (lookup_add_cases ??????? L)
23	[ * #E1 #E2 destruct
24	\| @IH
25	]
26	]
27	\| * #id1 #ty1 #tl #IH #stacksize #vartypes
28	whd in match (foldr ?????);
29	(* Avoid writing out the definition again *)
30	letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31	lapply (refl ? ih) whd in match ih; -ih
32	cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33	#vartypes' #stack' #FOLD #IH
34	whd in ⊢ (??(match % with [_⇒?])? → ?);
35	cases (orb ??)
36	#CHAR whd in CHAR:(??%?); destruct
37	#L cases (lookup_add_cases ??????? L)
38	[ 1,3: * #E1 #E2 destruct
39	#id' #n' #ty' #NE >lookup_add_miss /2/
40	#L' %1 -L -IH
41	generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42	generalize in match stack'; -stack'
43	elim tl
44	[ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45	elim globals in L';
46	[ normalize #E destruct
47	\| * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48	#L cases (lookup_add_cases ??????? L)
49	[ * #E1 #E2 destruct
50	\| @IH
51	]
52	]
53	\| * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55	#vartypes2 #stack2 #IH
56	whd in ⊢ (??%? → ?);
57	cases (orb ??)
58	[ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59	[ * #E1 #E2 destruct //
60	\| #L'' lapply (IH ?? (refl ??) L'') /2/
61	]
62	\| #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63	[ * #E1 #E2 destruct
64	\| #L'' lapply (IH ?? (refl ??) L'') /2/
65	]
66	]
67	]
68	\| -L #L #id' #n' #ty' #NE #L'
69	cases (lookup_add_cases ??????? L')
70	[ * #E1 #E2 destruct
71	%2 -IH -L'
72	generalize in match vartypes' in FOLD L; -vartypes'
73	generalize in match stack'; -stack'
74	elim tl
75	[ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76	elim globals in L;
77	[ normalize #E destruct
78	\| * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79	#L cases (lookup_add_cases ??????? L)
80	[ * #E1 #E2 destruct
81	\| @IH
82	]
83	]
84	\| * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85	whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86	#vartypes2 #stack2 #IH
87	whd in ⊢ (??%? → ?);
88	cases (orb ??)
89	#E whd in E:(??%?); destruct
90	#L cases (lookup_add_cases ??????? L)
91	[ 1,3: * #E1 #E2 destruct //
92	\| 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93	]
94	]
95	\| @(IH … (refl ??) L … NE)
96	]
97	\| -L #L #id' #n' #ty' #NE #L'
98	cases (lookup_add_cases ??????? L')
99	[ * #E1 #E2 destruct
100	\| @(IH … (refl ??) L … NE)
101	]
102	]
103	] qed.
104
105	(* And everything is in the stack frame. *)
106
107	lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108	characterise_vars globals f = 〈vartypes, stacksize〉 →
109	lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110	n + sizeof ty ≤ stacksize.
111	#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112	elim (args@vars)
113	[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114	whd in FOLD:(??%?); destruct elim globals in L;
115	[ #E normalize in E; destruct
116	\| * * #id' #r' #ty' #tl' #IH
117	whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118	[ * #E1 #E2 destruct
119	\| @IH
120	]
121	]
122	\| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123	whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124	#vartypes' #stackspace' #IH
125	whd in ⊢ (??(match % with [_⇒?])? → ?);
126	cases (orb ??) whd in ⊢ (??%? → ?);
127	#E destruct #L cases (lookup_add_cases ??????? L)
128	[ 1,3: * #E1 #E2 destruct //
129	\| 2,4: #L' lapply (IH … (refl ??) L') /2/
130	]
131	] qed.
132
133	(* Local variables show up in the variable characterisation as local. *)
134
135	lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
136	characterise_vars globals f = 〈vartypes, stacksize〉 →
137	Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
138	∃t. local_id vartypes id t.
139	#globals * #ret #args #vars #body
140	whd in match (characterise_vars ??); elim (args@vars)
141	[ #vartypes #stacksize #id #_ *
142	\| * #hd #ty #tl #IH
143	#vartypes #stacksize #id
144	whd in match (foldr ?????);
145	cases (foldr ? (Prod ??) ???) in IH ⊢ %;
146	#vartypes' #stackspace' #IH
147	whd in ⊢ (??(match % with [_⇒?])? → ?);
148	cases (orb ??)
149	#E whd in E:(??%?); destruct *
150	[ 1,3: #E destruct %{(typ_of_type ty)}
151	whd whd in match (lookup' ??); >lookup_add_hit //
152	\| 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
153	cases (identifier_eq ? id hd)
154	[ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
155	\| 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
156	]
157	]
158	] qed.
159
160	(* Put knowledge that Globals are global into a more useful form than the
161	one used for the invariant. *)
162
163	lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
164	characterise_vars globals f = 〈vartypes, stacksize〉 →
165	∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
166	Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
167	¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
168	#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
169	cases (characterise_vars_src … CHAR id ?)
170	[ * #r' * #ty' >L
171	* #E1 destruct (E1) #EX
172	%
173	[ @EX
174	\| % #EX' cases (characterise_vars_localid … CHAR EX')
175	#ty' whd in ⊢ (% → ?); >L *
176	]
177	\| * #ty' whd in ⊢ (% → ?); >L *
178	\| whd >(opt_eq_from_res ???? L) % #E destruct
179	] qed.
180
181
182	(* Show how the global environments match up. *)
183
184	lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
185	map_partial_All A B P f l H = OK ? l' →
186	All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
187	#A #B #P #f #l
188	elim l
189	[ #H #l' #MAP normalize in MAP; destruct //
190	\| #h #t #IH * #p #H #l'
191	whd in ⊢ (??%? → ?);
192	lapply (refl ? (f h p)) whd in match (proj1 ???);
193	cases (f h p) in ⊢ (???% → %);
194	[ #b #E #MAP cases (bind_inversion ????? MAP)
195	#tl' * #MAP' #E' normalize in E'; destruct
196	% [ %{p} @E \| @IH [ @H \| @MAP' ] ]
197	\| #m #_ #X normalize in X; destruct
198	]
199	] qed.
200
201
202	definition clight_cminor_matching : clight_program → matching ≝
203	λp.
204	let tmpuniverse ≝ universe_for_program p in
205	let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
206	let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
207	let globals ≝ fun_globals @ var_globals in
208	mk_matching
209	?? (list init_data × type) (list init_data)
210	(λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
211	(λv,w. \fst v = w).
212
213	lemma clight_to_cminor_varnames : ∀p,p'.
214	clight_to_cminor p = OK ? p' →
215	prog_var_names … p = prog_var_names … p'.
216	* #vars #fns #main * #vars' #fns' #main'
217	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
218	whd in E:(??%%); destruct
219	-MAP normalize
220	elim vars
221	[ //
222	\| * * #id #r * #d #t #tl #IH normalize >IH //
223	] qed.
224
225
226	lemma clight_to_cminor_matches : ∀p,p'.
227	clight_to_cminor p = OK ? p' →
228	match_program (clight_cminor_matching p) p p'.
229	* #vars #fns #main * #vars' #fns' #main'
230	#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
231	whd in E:(??%%); destruct
232	%
233	[ -MAP whd in match (m_V ?); whd in match (m_W ?);
234	elim vars
235	[ //
236	\| * * #id #r * #init #ty #tl #IH %
237	[ % //
238	\| @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
239	]
240	]
241	\| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
242	* #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
243	normalize in E; destruct
244	<(clight_to_cminor_varnames … TO)
245	% whd
246	% [2: % [2: @TRANSF \| skip ] \| skip ]
247	\| %
248	] qed.
249
250	include "Clight/Cexec.ma".
251	include "Clight/abstract.ma".
252	include "Cminor/abstract.ma".
253
254	(* Invariants used in simulation *)
255
256	record clight_cminor_inv : Type[0] ≝ {
257	globals : list (ident × region × type);
258	ge_cl : genv_t clight_fundef;
259	ge_cm : genv_t (fundef internal_function);
260	eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
261	trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
262	∃tmp_u,f',H1,H2.
263	translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
264	find_funct … ge_cm v = Some ? f'
265	}.
266
267	include "Clight/CexecInd.ma".
268	include "Clight/frontend_misc.ma".
269	include "Clight/memoryInjections.ma".
270
271	lemma intsize_eq_inversion :
272	∀sz,sz'.
273	∀A:Type[0].
274	∀ok,not_ok.
275	intsize_eq_elim' sz sz' (λsz,sz'. res A)
276	(OK ? ok)
277	(Error ? not_ok) = (OK ? ok) →
278	sz = sz'.
279	* * try // normalize
280	#A #ok #not_ok #Habsurd destruct
281	qed.
282
283	(* Perhaps we will have to be more precise on what is allocated, etc.
284	cf [exec_alloc_variables]. For now this is conveniently hidden in
285	the [value_eq E v v'] *)
286	definition memory_matching ≝
287	λE:embedding.
288	λm,m':mem.
289	λen:cl_env.
290	λvenv:cm_env.
291	λcminv:clight_cminor_inv.
292	λsp:block.
293	λvars:var_types.
294	∀id.
295	match lookup SymbolTag ? en id with
296	[ None ⇒
297	match find_symbol ? (ge_cl cminv) id with
298	[ None ⇒ True
299	\| Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
300	]
301	\| Some cl_blo ⇒
302	match lookup ?? vars id with
303	[ Some kind ⇒
304	let 〈vtype, type〉 ≝ kind in
305	match vtype with
306	[ Stack n ⇒
307	E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
308	\| Local ⇒
309	∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
310	∃v'. lookup ?? venv id = Some ? v' ∧
311	value_eq E v v'
312	\| _ ⇒ False ]
313	\| None ⇒ False ]
314	].
315
316	lemma type_should_eq_inversion :
317	∀ty1,ty2,P,f,res.
318	type_should_eq ty1 ty2 P f = OK ? res →
319	ty1 = ty2 ∧ f ≃ res.
320	#ty1 #ty2 #P #f #res normalize
321	cases (type_eq_dec ty1 ty2) normalize nodelta
322	[ 2: #Hneq #Habsurd destruct ]
323	#Heq #Heq2 @conj try assumption
324	destruct (Heq2) cases Heq normalize nodelta
325	@eq_to_jmeq @refl
326	qed.
327
328	lemma load_value_of_type_by_ref :
329	∀ty,m,b,off,val.
330	load_value_of_type ty m b off = Some ? val →
331	typ_of_type ty ≃ ASTptr →
332	access_mode ty ≃ By_reference →
333	val = Vptr (mk_pointer b off).
334	*
335	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
336	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
337	#m #b #off #val
338	[ 1,6,7: normalize #Habsurd destruct (Habsurd)
339	\| 4,5: normalize #Heq #_ #_ destruct @refl
340	\| 2: #_ normalize #Heq destruct
341	\| *: #Hload normalize #_ #H
342	lapply (jmeq_to_eq ??? H) #Heq destruct
343	] qed.
344
345	lemma load_value_of_type_by_value :
346	∀ty,m,b,off,val.
347	access_mode ty = By_value (typ_of_type ty) →
348	load_value_of_type ty m b off = Some ? val →
349	loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
350	*
351	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
352	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
353	#m #b #off #val
354	normalize in match (access_mode ?);
355	[ 1,4,5,6,7: #Habsurd destruct ]
356	#_
357	#H @H
358	qed.
359
360	include "Clight/CexecSound.ma".
361
362	lemma lookup_exec_alloc :
363	∀source_variables, initial_env, env, var_id, clb, m, m'.
364	lookup ?? env var_id = Some ? clb →
365	exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
366	lookup ?? initial_env var_id = Some ? clb ∨
367	Exists ? (λx. \fst x = var_id) source_variables.
368	#source_variables
369	elim source_variables
370	[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
371	destruct (Hexec_alloc) %1 @Hlookup
372	\| 2: * #id #ty #tail #Hind
373	#init_env #env #var #clb #m #m' #Hlookup
374	whd in ⊢ (??%? → ?);
375	cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
376	#Hexec_alloc
377	@(match identifier_eq ? id var with [ inl Heq ⇒ ? \| inr Hneq ⇒ ? ])
378	[ 1: destruct (Heq) %2 %1 @refl ]
379	cases (Hind … Hlookup Hexec_alloc)
380	[ @cthulhu (* standard reasoning on positive_maps. check lib. *)
381	\| #Hexists %2 %2 @Hexists ]
382	] qed.
383
384	lemma characterise_vars_lookup_local :
385	∀globals,f,vartypes,stacksize,id,clb,env.
386	characterise_vars globals f = 〈vartypes, stacksize〉 →
387	lookup ?? env id = Some ? clb →
388	(∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
389	∃t. local_id vartypes id t.
390	#globals #f #vartypes #stacksize #id #clb #env
391	#Hchar #Hlookup * #m * #m' #Hexec
392	cases (lookup_exec_alloc … Hlookup Hexec)
393	[ normalize in ⊢ (% → ?); #Heq destruct
394	\| @(characterise_vars_localid … Hchar) ]
395	qed.
396
397
398	lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
399	(∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
400	lookup ?? env' var_id = None ? →
401	lookup ?? env var_id = None ? ∧
402	¬(Exists (ident×type) (λx:ident×type.\fst x=var_id) variables).
403	#vars elim vars
404	[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
405	#H @conj try @H % //
406	\| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
407	whd in ⊢ ((??%?) → ? → ?);
408	cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
409	normalize nodelta #Hexec #Hlookup
410	lapply (Hind … (ex_intro … (ex_intro … Hexec)) Hlookup)
411	cases env #env cases id' #id' cases var #var normalize
412	@(eqb_elim … id' var)
413	[ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
414	#Heq <Heq @conj try @Hlookup' % *
415	[ #Heq' destruct (Heq') cases Hneq #H @H @refl
416	\| cases Hexists' #H @H ]
417	\| 1: #Heq destruct (Heq) * #Hlookup' #Hexists'
418	lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
419	>H1 in Hlookup'; #Heq destruct
420	]
421	] qed.
422
423	lemma variable_not_in_env_but_in_vartypes_is_global :
424	∀env,env',f,vars,stacksize,globals,var_id.
425	(∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
426	characterise_vars globals f =〈vars,stacksize〉 →
427	lookup ?? env' var_id = None ? →
428	∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
429	∃r.allocty = Global r.
430	#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
431	#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
432	lapply (characterise_vars_src … Hcharacterise var_id ?)
433	[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
434	#Hlookup >Hlookup #_ #Habsurd destruct ]
435	*
436	[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
437	>Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
438	* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
439	@(match allocty
440	return λx. allocty = x → ?
441	with
442	[ Global r ⇒ λ_. ?
443	\| Stack st' ⇒ λHalloc. ?
444	\| Local ⇒ λHalloc. ?
445	] (refl ? allocty))
446	[ @False_ind ] normalize nodelta
447	#Heq_typ
448	(* Halloc is in contradiction with Hlookup_fail *)
449	lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
450	* #Hlookup' #Hnot_exists
451	lapply (characterise_vars_all … Hcharacterise var_id t ?)
452	[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
453	#Hexists @False_ind
454	cut (Exists (ident×type) (λx:ident×type.\fst x=var_id) (fn_params f@fn_vars f))
455	[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
456	* #id' #ty' #tl #Hind *
457	[ 1,3: * #Heq #_ %1 @Heq
458	\| *: #H %2 @Hind @H ] ]
459	#H cases Hnot_exists #H' @H' @H
460	qed.
461
462	lemma intsize_eq_elim_dec :
463	∀sz1,sz2.
464	∀P: ∀sz1,sz2. Type[0].
465	((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
466	((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
467	* * #P normalize
468	try /3 by or_introl, conj, refl/
469	%2 @conj try //
470	% #H destruct
471	qed.
472
473	lemma typ_eq_elim :
474	∀t1,t2.
475	∀(P: (t1=t2)+(t1≠t2) → Prop).
476	(∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
477	#t1 #t2 #P #Hl #Hr
478	@(match typ_eq t1 t2
479	with
480	[ inl H ⇒ Hl H
481	\| inr H ⇒ Hr H ])
482	qed.
483
484
485	lemma translate_notbool_to_cminor :
486	∀t,sg,arg.
487	∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
488	∀res. sem_unary_operation Onotbool arg t = Some ? res →
489	eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
490	*
491	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
492	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
493	normalize in match (typ_of_type ?);
494	#sg #arg #cmop
495	whd in ⊢ (??%% → ?); #Heq destruct (Heq)
496	cases arg
497	[ \| #vsz #vi \| \| #vp
498	\| \| #vsz #vi \| \| #vp
499	\| \| #vsz #vi \| \| #vp
500	\| \| #vsz #vi \| \| #vp
501	\| \| #vsz #vi \| \| #vp
502	\| \| #vsz #vi \| \| #vp
503	\| \| #vsz #vi \| \| #vp
504	\| \| #vsz #vi \| \| #vp ]
505	#res
506	whd in ⊢ ((??%?) → ?);
507	#Heq
508	[ 6,11,12: \| *: destruct (Heq) ]
509	[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
510	\| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
511	#H normalize nodelta #Heq destruct
512	whd in match (eval_unop ????);
513	cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
514	] qed.
515
516	lemma translate_notint_to_cminor :
517	∀t,t',arg.
518	∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
519	∀res. sem_unary_operation Onotint arg t = Some ? res →
520	eval_unop (typ_of_type t) t' cmop arg = Some ? res.
521	#ty *
522	[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
523	#sz #sg #arg #cmop
524	whd in match (translate_unop ???);
525	@(match typ_eq (ASTint sz sg) (typ_of_type ty)
526	with
527	[ inl H ⇒ ?
528	\| inr H ⇒ ? ])
529	normalize nodelta
530	[ 2: #Heq destruct ]
531	lapply H -H
532	lapply cmop -cmop
533	cases ty
534	[ \| #sz' #sg' \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
535	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
536	normalize nodelta
537	#cmop normalize in match (typ_of_type ?); #H destruct
538	#H' normalize in H';
539	destruct (H')
540	#res
541	whd in match (sem_unary_operation ???);
542	cases arg
543	[ \| #vsz #vi \| \| #vp
544	\| \| #vsz #vi \| \| #vp
545	\| \| #vsz #vi \| \| #vp
546	\| \| #vsz #vi \| \| #vp ]
547	whd in match (sem_notint ?);
548	#H destruct (H) @refl
549	qed.
550
551
552	lemma translate_negint_to_cminor :
553	∀t,t',arg.
554	∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
555	∀res. sem_unary_operation Oneg arg t = Some ? res →
556	eval_unop (typ_of_type t) t' cmop arg = Some ? res.
557	#ty *
558	[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
559	#sz #sg #arg #cmop
560	whd in match (translate_unop ???);
561	@(match typ_eq (ASTint sz sg) (typ_of_type ty)
562	with
563	[ inl H ⇒ ?
564	\| inr H ⇒ ? ])
565	normalize nodelta
566	[ 2: #Heq destruct ]
567	lapply H -H
568	lapply cmop -cmop
569	cases ty
570	[ \| #sz' #sg' \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
571	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
572	normalize nodelta
573	#cmop normalize in match (typ_of_type ?); #H destruct
574	#H' normalize in H';
575	destruct (H')
576	#res
577	whd in match (sem_unary_operation ???);
578	cases arg
579	[ \| #vsz #vi \| \| #vp
580	\| \| #vsz #vi \| \| #vp
581	\| \| #vsz #vi \| \| #vp
582	\| \| #vsz #vi \| \| #vp ]
583	whd in match (sem_neg ??);
584	#H destruct (H)
585	whd in match (eval_unop ????);
586	cases (eq_intsize sz' vsz) in H; normalize nodelta
587	#H destruct @refl
588	qed.
589
590
591	lemma translate_unop :
592	∀ty,sg,op,cmop.
593	translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
594	∀arg,res. sem_unary_operation op arg ty = Some ? res →
595	eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
596	#ty #sg * #cmop #Htranslate #arg
597	[ @translate_notbool_to_cminor assumption
598	\| @translate_notint_to_cminor assumption
599	\| @translate_negint_to_cminor assumption ]
600	qed.
601
602	lemma classify_add_inversion :
603	∀ty1,ty2.
604	(∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
605	(∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
606	(∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
607	(classify_add ty1 ty2 = add_default ty1 ty2).
608	#ty1 #ty2
609	cases (classify_add ty1 ty2)
610	[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
611	\| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
612	\| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
613	\| #tya #tyb %2 @refl ]
614	qed.
615
616	lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2.
617	* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
618	[ 4: #P #a #x normalize #H destruct (H) @refl
619	\| 3: cases sz cases sg #P #A #x normalize #H destruct
620	\| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
621	cases sz cases sz2 cases sg cases sg2
622	#P #a #x #H normalize in H:(??%?); destruct (H)
623	try @refl
624	qed.
625
626	lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
627	*
628	[ * * normalize @refl
629	\| @refl ]
630	qed.
631
632	lemma intsize_eq_elim_inversion :
633	∀A:Type[0].
634	∀sz1,sz2.
635	∀elt1,f,errmsg,res.
636	intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
637	∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
638	#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
639	%{(refl ??)} normalize nodelta >H @refl
640	qed.
641
642	lemma eval_expr_sim :
643	∀(inv:clight_cminor_inv).
644	∀(f:function).
645	∀(vars:var_types).
646	∀stacksize.
647	characterise_vars (globals inv) f = 〈vars, stacksize〉 →
648	∀(cl_env:cl_env).
649	(∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
650	∀(cl_m:mem).
651	∀(cm_env:cm_env).
652	∀(sp:block).
653	∀(cm_m:mem).
654	∀E:embedding.
655	∀minj:memory_inj E cl_m cm_m.
656	memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
657	(* clight expr to cminor expr *)
658	(∀(e:expr).
659	∀(e':CMexpr (typ_of_type (typeof e))).
660	∀Hexpr_vars.
661	translate_expr vars e = OK ? («e', Hexpr_vars») →
662	∀cl_val,trace,Hyp_present.
663	exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
664	∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
665	value_eq E cl_val cm_val) ∧
666	(* clight /lvalue/ to cminor /expr/ *)
667	(∀ed,ty.
668	∀(e':CMexpr ASTptr).
669	∀Hexpr_vars.
670	translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
671	∀cl_blo,cl_off,trace,Hyp_present.
672	exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
673	∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
674	value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
675	#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
676	@expr_lvalue_ind_combined
677	[ 1: (* Integer constant *)
678	#csz #ty cases ty
679	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
680	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
681	#i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
682	#val #trace #Hpresent #Hexec_cl
683	whd in Htranslate:(??%?);
684	[ 1,3,4,5,6,7,8: destruct ]
685	cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars))))
686	[ 2: * #H_err #H_neq_sz
687	lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
688	>Htranslate #Habsurd destruct (Habsurd) ]
689	* #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
690	destruct (Heq_sz)
691	>Htranslate -Htranslate -H_ok #Heq destruct (Heq)
692	whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
693	#Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
694	\| 2: *
695	[ #sz #i \| #var_id \| * #ed1 #ty1 \| #e1 \| #op #e1 \| #op #e1 #e2 \| #cast_ty #e1
696	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
697	try /2 by I/
698	#ty whd in ⊢ (% → ?); #Hind
699	whd in match (Plvalue ???);
700	whd in match (typeof ?);
701	#cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
702	whd in Hexec:(??%?);
703	whd in match (exec_lvalue' ?????) in Hexec:(??%?);
704	cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
705	whd in Hcl_success:(???%);
706	[ 1: (* var case *)
707	lapply Hcl_success -Hcl_success -Hind
708	(* Peform case analysis on presence of variable in local Clight env.
709	* if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
710	@(match lookup SymbolTag block cl_env var_id
711	return λx.(lookup SymbolTag block cl_env var_id = x) → ?
712	with
713	[ None ⇒ λHcl_lookup. ?
714	\| Some loc ⇒ λHcl_lookup. ?
715	] (refl ? (lookup SymbolTag block cl_env var_id)))
716	normalize nodelta
717	[ 1: (* global case *)
718	#Hlookup_global
719	cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
720	* #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
721	#Heq whd in Heq:(???%); destruct (Heq)
722	lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
723	* #var_id_alloctype * #var_id_type * #Heq
724	cases (variable_not_in_env_but_in_vartypes_is_global …
725	Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
726	#r #Heq' destruct (Heq') normalize nodelta
727	lapply Hcl_load_success -Hcl_load_success
728	lapply Hyp_present -Hyp_present
729	lapply Hexpr_vars -Hexpr_vars
730	lapply cm_expr -cm_expr inversion (access_mode ty)
731	[ #typ_of_ty \| \| #typ_of_ty ]
732	#Heq_typ_of_type #Heq_access_mode
733	#cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
734	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
735	whd in match (eval_expr ???????);
736	whd in match (eval_expr ???????);
737	whd in match (eval_constant ????);
738	<(eq_sym … inv) >Hfind_symbol normalize nodelta
739	cases (bind_inversion ????? Hcl_load_success) #x *
740	#Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
741	lapply (opt_to_res_inversion ???? Hopt_to_res)
742	#Hcl_load_success
743	[ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
744	@conj try @refl
745	whd in Hcm_load_success:(??%?);
746	lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
747	>(load_value_of_type_by_ref … Hcl_load_success)
748	try assumption %4
749	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
750	>Hfind_symbol normalize nodelta #Heq_embedding
751	whd in match (shift_offset ???);
752	>addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
753	normalize nodelta @refl
754	\| 1: cut (access_mode ty=By_value (typ_of_type ty))
755	[ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
756	lapply Heq_access_mode <Heqt // ] #Haccess
757	lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
758	#Hvalid_ptr
759	lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
760	[ whd in ⊢ (??%?);
761	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
762	>Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
763	* #val' * #Hcm_load_success #Hvalue_eq
764	lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
765	#Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
766	normalize %{val'} @conj try @refl assumption ]
767	\| 2: (* local case *)
768	#Heq destruct (Heq)
769	lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
770	* #var_id_alloc_type * #var_id_type *
771	generalize in match var_id_alloc_type; * normalize nodelta
772	[ 1: #r #Hlookup_vartype
773	lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
774	* #typ whd in match (local_id ???);
775	>Hlookup_vartype normalize nodelta @False_ind
776	\| 2: (* Stack local *)
777	lapply Hcl_load_success -Hcl_load_success
778	lapply Hyp_present -Hyp_present
779	lapply Hexpr_vars -Hexpr_vars
780	lapply cm_expr -cm_expr inversion (access_mode ty)
781	[ #typ_of_ty \| \| #typ_of_ty ]
782	#Heq_typ_of_type #Heq_access_mode
783	#cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
784	#stack_depth #Hlookup_vartype_success normalize nodelta
785	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
786	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
787	cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
788	* #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
789	>Hlookup' normalize nodelta #Hembedding_eq
790	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
791	#loaded_val * #Hload_val
792	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
793	lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
794	#Hload_success whd in match (eval_expr ???????);
795	cut (pointer_translation (mk_pointer cl_b zero_offset) E =
796	Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
797	[ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
798	>offset_plus_0 @refl ]
799	#Hpointer_translation
800	[ 2: (* By-ref *)
801	whd in Hload_success:(??%?);
802	lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
803	#Heq_val
804	>Heq_val
805	%{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
806	@conj try @refl
807	%4 whd in match (shift_offset ???);
808	whd in match zero_offset;
809	>commutative_addition_n >addition_n_0 @Hpointer_translation
810	\| 1: (* By value *)
811	lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0
812	lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
813	[ @(load_by_value_success_valid_pointer … Hload_success)
814	lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
815	* #cm_val * #Hload_in_cm #Hvalue_eq
816	%{cm_val} @conj try assumption
817	lapply (load_value_of_type_by_value … Hload_in_cm)
818	[ lapply Heq_access_mode <Heq0 #Heq1
819	@(jmeq_to_eq ??? Heq1) ]
820	#Hloadv <Heq0
821	whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
822	>Hloadv @refl ]
823	\| 3: (* Register local variable *)
824	#Hlookup_eq
825	lapply (res_inversion ?????? Hlookup_eq)
826	* * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
827	#Htype_eq
828	cases (type_should_eq_inversion
829	var_id_type
830	ty
831	(λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
832	… Htype_eq) -Htype_eq
833	(* Reverting all premises in order to perform type rewrite *)
834	#Htype_eq
835	lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
836	lapply Hcl_load_success -Hcl_load_success
837	lapply Hcl_lookup -Hcl_lookup
838	lapply Hyp_present -Hyp_present
839	lapply Hexpr_vars -Hexpr_vars
840	lapply cm_expr
841	destruct (Htype_eq)
842	#cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
843	#Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
844	destruct (Hexpr_eq)
845	whd in match (eval_expr ???????);
846	whd in match (lookup_present ?????);
847	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
848	>Hlookup' normalize nodelta #Hmatching
849	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
850	#loaded_val * #Hload_val
851	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
852	lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
853	#Hload_success
854	cases (Hmatching … Hload_success) #val'
855	* #Hlookup_in_cm #Hvalue_eq %{val'}
856	cases Hyp_present
857	>Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
858	(* seems ok *)
859	]
860	]
861	\| 2: lapply Hcl_success -Hcl_success
862	lapply Htranslate_expr -Htranslate_expr
863	lapply Hind -Hind cases ty1
864	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
865	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ]
866	#Hind #Htranslate_expr #Hexec_cl
867	cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
868	* whd in match (typ_of_type ?); normalize nodelta
869	#cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
870	whd in ⊢ ((???%) → ?);
871	[ 1,2,6,7: #Heq destruct (Heq) ]
872	lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
873	whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
874	#Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
875	[ 1,3,5,7: @cthulhu ]
876	whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
877	cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
878	#Hexec_cl_ind #Hcl_ptr
879	cut (∃ptr. cl_ptr = Vptr ptr)
880	[ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
881	#H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
882	* * #cl_ptr_block #cl_ptr_off -Hcl_ptr
883	#Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
884	#Hind lapply (Hind (refl ??)) -Hind
885	* #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
886	lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
887	destruct (Hcm_ptr) #Hpointer_translation
888	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
889	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
890	-Hopt_to_res
891	lapply Hyp_present -Hyp_present
892	lapply Hexpr_vars -Hexpr_vars
893	lapply cm_expr -cm_expr
894	inversion (access_mode ty)
895	[ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
896	lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
897	#cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
898	#Heq destruct (Heq)
899	[ 1,2,3,4: (* By_value *)
900	(* project Hcl_load_success in Cminor through memory_inj *)
901	lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
902	[ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
903	* #cm_val * #Hcm_load_success #Hvalue_eq
904	lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
905	#Hloadv_cm
906	whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
907	>Hloadv_cm normalize %{cm_val} @conj try @refl assumption
908	\| : ( By reference *)
909	>Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
910	lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
911	#Hval >Hval %4 assumption ]
912	\| 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
913	lapply (refl ? (typeof e1))
914	cases (typeof e1) in ⊢ ((???%) → %);
915	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
916	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ] normalize nodelta
917	#Heq_typeof normalize nodelta
918	[ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
919	whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
920	normalize nodelta #Htranslate_expr
921	cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
922	* whd in match (typ_of_type ?); normalize nodelta
923	#cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
924	[ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
925	#cm_field_off * #Hcm_field_off
926	\| lapply Htranslate_expr2 -Htranslate_expr2 ]
927	cases (bind_inversion ????? Hexec_cl) -Hexec_cl
928	* * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
929	whd in Hexec_lvalue:(???%);
930	[ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
931	#cl_field_off * #Hcl_field_off #Hoffset_eq ]
932	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
933	#cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
934	lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
935	[ (* Struct case *)
936	lapply Hcl_load_value -Hcl_load_value
937	lapply Hyp_present -Hyp_present
938	lapply Hexpr_vars -Hexpr_vars
939	lapply cm_expr -cm_expr
940	lapply Hind -Hind
941	cases ty
942	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
943	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
944	#Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
945	normalize nodelta
946	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
947	whd in match (eval_expr ???????);
948	(* applying the arguments of the induction hypothesis progressively *)
949	lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
950	(Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
951	[ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
952	lapply (Hind ?)
953	[ 1,3,5,7,9:
954	whd in ⊢ (??%?); >Heq_typeof normalize nodelta
955	>Htranslate_expr_ind whd in match (m_bind ?????);
956	>Hcm_field_off normalize nodelta @refl ] -Hind #Hind
957	whd in Hoffset_eq:(???%); destruct (offset_eq)
958	cut (cl_field_off = cm_field_off)
959	[ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
960	normalize #Heq destruct (Heq) @refl ]
961	#Heq destruct (Heq)
962	lapply (Hind cl_b cl_o trace ?)
963	[ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
964	lapply (Hind ?) -Hind
965	[ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
966	>Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
967	@Hoffset_eq ]
968	* #cm_val' * #Heval_expr #Hvalue_eq
969	lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
970	* #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
971	[ 1,2,5: (* by-value *)
972	lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
973	[ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
974	* #cm_val * #Hcm_load_value #Hvalue_eq
975	lapply (load_value_of_type_by_value … Hcm_load_value)
976	[ 1,3,5: @refl ]
977	#Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
978	try @refl try assumption
979	\| 3,4: (* by-ref *)
980	whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
981	%{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
982	whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
983	]
984	\| (* union case *)
985	lapply Hcl_load_value -Hcl_load_value
986	lapply Hyp_present -Hyp_present
987	lapply Hexpr_vars -Hexpr_vars
988	lapply cm_expr -cm_expr
989	lapply Hind -Hind
990	cases ty
991	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
992	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
993	whd in match (typ_of_type ?); normalize nodelta
994	#Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
995	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
996	[ 1,2,5: (* by-value *)
997	whd in match (eval_expr ???????);
998	lapply (Hind cm_expr_ind Hexpr_vars ?)
999	[ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
1000	whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1001	-Hind #Hind
1002	lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
1003	whd in match (m_bind ?????); #Hind
1004	cases (Hind (refl ??)) -Hind
1005	#cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
1006	cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
1007	destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
1008	lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
1009	[ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1010	* #cm_val * #Hcm_load_value #Hvalue_eq
1011	lapply (load_value_of_type_by_value … Hcm_load_value)
1012	[ 1,3,5: @refl ]
1013	#Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
1014	try @refl assumption
1015	\| 3,4:
1016	whd in Hexec_cl:(???%); destruct (Hexec_cl)
1017	lapply (Hind cm_expr Hexpr_vars)
1018	whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
1019	lapply (Hind Htranslate_expr_ind) -Hind
1020	whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1021	>Hexec_lvalue whd in match (m_bind ?????);
1022	#Hind cases (Hind … Hyp_present (refl ??))
1023	#cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
1024	try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
1025	assumption ]
1026	]
1027	]
1028	\| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
1029	whd in Hexec_lvalue_var:(??%?);
1030	(* check whether var is local or global *)
1031	lapply (Hlocal_matching var)
1032	lapply (variable_not_in_env_but_in_vartypes_is_global … var Hexec_alloc … Hcharacterise)
1033	cases (lookup ?? cl_env var) in Hexec_lvalue_var;
1034	normalize nodelta
1035	[ 1: (* global *)
1036	#Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
1037	cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
1038	whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
1039	lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
1040	#Hembed
1041	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1042	* #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
1043	cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
1044	normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1045	whd in match (eval_expr ???????);
1046	whd in match (eval_constant ????);
1047	<(eq_sym inv var) >Hfind_symbol normalize nodelta
1048	%{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1049	@conj try @refl %4 whd in match (pointer_translation ??);
1050	>Hembed normalize nodelta whd in match (shift_offset ???);
1051	>addition_n_0 @refl
1052	\| 2: (* local *)
1053	#BL #Heq destruct (Heq) #_
1054	@(match (lookup ?? vars var)
1055	return λx. (lookup ?? vars var = x) → ?
1056	with
1057	[ None ⇒ ?
1058	\| Some kind ⇒ ?
1059	] (refl ??))
1060	normalize nodelta
1061	#Hlookup [ @False_ind ]
1062	cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
1063	#Hlookup
1064	lapply (refl ? var_alloctype)
1065	cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
1066	[ #reg #Heq @False_ind \| #stacksize #Hvar_alloc #Hembed \| #Hvar_alloc #Hlookup' ]
1067	[ (* stack alloc*)
1068	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1069	* #var_alloctype' #var_type' * #Hlookup_vartype'
1070	whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1071	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1072	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
1073	%{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
1074	@conj try @refl %4 whd in match (pointer_translation ??);
1075	>Hembed @refl
1076	\| (* local alloc *)
1077	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1078	* #var_alloctype' #var_type' * #Hlookup_vartype'
1079	whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1080	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1081	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
1082	(\| 4: #e #ty)
1083	\| 4:
1084	* #ed #ety cases ety
1085	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
1086	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ] normalize nodelta
1087	whd in match (typeof ?);
1088	#ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
1089	cases (bind_inversion ????? Htranslate) -Htranslate
1090	* #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1091	cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1092	* #cl_val #trace0 * #Hexec_expr #Hcl_val
1093	whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
1094	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1095	cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
1096	[ 1,3,5,7: cases cl_val in Hcl_val; normalize
1097	[ 1,5,9,13: #Heq destruct (Heq)
1098	\| 2,6,10,14: #sz #vec #Heq destruct (Heq)
1099	\| 3,7,11,15: #Heq destruct (Heq)
1100	\| 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
1101	* #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
1102	cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
1103	#cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
1104	%{cm_val} @conj try @refl try assumption
1105	\| 5:
1106	#ty cases ty
1107	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1108	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1109	#ed #ty' #Hind
1110	whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
1111	#Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1112	cases (bind_inversion ????? Htranslate) -Htranslate
1113	* #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1114	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1115	* * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
1116	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1117	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1118	cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
1119	#cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
1120	%{cm_val} @conj try @refl assumption
1121	\| 6:
1122	#ty *
1123	[ cases ty
1124	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1125	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1126	#e #Hind
1127	whd in match (typeof ?);
1128	#e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
1129	#Htranslate
1130	[ 3,4,5,8: destruct (Htranslate)
1131	\| 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1132	cases sz normalize nodelta
1133	#e' #Hexpr_vars #Htranslate
1134	[ 1, 2: destruct (Htranslate) ] ]
1135	#cl_val #trace #Hyp_present #Hexec_expr
1136	cases (bind_inversion ????? Htranslate) -Htranslate
1137	#cmop * #Htranslate_unop #Hexec_arg
1138	cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1139	* #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1140	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1141	* #cl_arg #cl_trace * #Hexec_cl
1142	whd in ⊢ ((???%) → ?); #Hexec_unop
1143	cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1144	#v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1145	lapply (opt_to_res_inversion ???? Hopt) -Hopt
1146	#Hsem_cl whd in match (eval_expr ???????);
1147	cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1148	#cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1149	lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
1150	* #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
1151	whd in match (typ_of_type Tvoid);
1152	lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
1153	#H >H @refl
1154	\| *:
1155	cases ty
1156	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id
1157	\| \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1158	#e #Hind whd in match (typeof ?); whd in match (typ_of_type ?);
1159	#e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
1160	whd in Htranslate:(??%?);
1161	[ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
1162	cases (bind_inversion ????? Htranslate) -Htranslate
1163	#cmop * #Htranslate_unop #Hexec_arg
1164	cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1165	* #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1166	cases (bind_inversion ????? Hexec) -Hexec
1167	* #cl_arg #cl_trace * #Hexec_cl
1168	whd in ⊢ ((???%) → ?); #Hexec_unop
1169	cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1170	#v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1171	lapply (opt_to_res_inversion ???? Hopt) -Hopt
1172	#Hcl_unop whd in match (eval_expr ???????);
1173	cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1174	#op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1175	lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
1176	* #op_res * #Hcl_sem #Hvalue_eq
1177	[ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
1178	%{op_res} @conj try @refl assumption
1179	\| 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
1180	%{op_res} @conj try @refl assumption
1181	]
1182	]
1183	\| 7: (* binary ops *)
1184	#ty
1185	letin s ≝ (typ_of_type ty)
1186	#op #e1 #e2
1187	#Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
1188	cases (bind_inversion ????? Htranslate) -Htranslate
1189	* #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
1190	cases (bind_inversion ????? Htranslate) -Htranslate
1191	* #rhs #Hexpr_vars_rhs * #Htranslate_rhs
1192	whd in ⊢ ((??%?) → ?);
1193	cases op whd in match (translate_binop ??????);
1194	@cthulhu (* PITA *)
1195	\| 8: #ty #ty' * #ed #ety
1196	cases ety
1197	[ \| #esz #esg \| #eptr_ty \| #earray_ty #earray_sz \| #edomain #ecodomain
1198	\| #estructname #efieldspec \| #eunionname #efieldspec \| #eid ]
1199	whd in match (typeof ?); whd in match (typ_of_type ?);
1200	#Hind whd in match (typeof ?);
1201	#cm_expr #Hexpr_vars #Htranslate
1202	cases (bind_inversion ????? Htranslate) -Htranslate
1203	* #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
1204	cases (bind_inversion ????? Htranslate) -Htranslate
1205	* #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate
1206	[ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
1207	cases (bind_inversion ????? Htranslate) -Htranslate
1208	* #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
1209	#Heq destruct (Heq)
1210	#cl_val #trace #Hyp_present #Hexec_cm
1211	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1212	* #cm_val #trace0 * #Hexec_cm #Hexec_cast
1213	cases (bind_inversion ????? Hexec_cast) -Hexec_cast
1214	#cast_val * #Hexec_cast
1215	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1216	lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq
1217	lapply Hexec_cast -Hexec_cast
1218	lapply Htyp_should_eq -Htyp_should_eq
1219	lapply Htranslate_cast -Htranslate_cast
1220	lapply Hexpr_vars_cast -Hexpr_vars_cast
1221	lapply cm_cast -cm_cast
1222	lapply Hyp_present -Hyp_present
1223	lapply Hexpr_vars -Hexpr_vars
1224	lapply cm_expr -cm_expr
1225	<Htype_eq -Htype_eq
1226	whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta
1227	cases ty'
1228	[ \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id'
1229	\| \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id'
1230	\| \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id' ]
1231	#cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast
1232	whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee;
1233	whd in match (typeof ?) in Htranslate_cast Hexec_cast;
1234	#Heq destruct (Heq)
1235	whd in Htranslate_cast:(??%%);
1236	whd in Hexpr_vars;
1237	destruct (Htranslate_cast)
1238	[ 1,2,3,4,7:
1239	lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1240	* #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast
1241	lapply Hvalue_eq -Hvalue_eq lapply Hexec_cm -Hexec_cm
1242	whd in Hexec_cast:(??%%);
1243	cases cm_val in Hexec_cast; normalize nodelta
1244	[ \| #vsz #vi \| \| #vp
1245	\| \| #vsz #vi \| \| #vp
1246	\| \| #vsz #vi \| \| #vp
1247	\| \| #vsz #vi \| \| #vp
1248	\| \| #vsz #vi \| \| #vp ]
1249	[ 2,6,10,14,18:
1250	\| *: #Habsurd destruct (Habsurd) ]
1251	#Hexec_cast #Hexec_cm #Hvalue_eq
1252	[ 1,2,3:
1253	cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
1254	#Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
1255	[ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
1256	[ 1,2,4,5:
1257	cases (bind_inversion ????? Hexec_cast)
1258	whd in match (typeof ?);
1259	#cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
1260	whd in match (eq_rect_r ??????);
1261	[ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
1262	@(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
1263	[ 2,4: #foo #Habsurd destruct (Habsurd) ]
1264	#Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
1265	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1266	whd in match (typ_of_type ?); whd in match (eval_expr ???????);
1267	>Heval_castee normalize nodelta whd in match (eval_unop ????);
1268	>(value_eq_int_inversion … Hvalue_eq) normalize nodelta
1269	>Heq_vi >eq_bv_true normalize
1270	%{Vnull} @conj try @refl %3
1271	\| 3: destruct (Hcl_val_eq)
1272	whd in match (eval_expr ???????);
1273	>Heval_castee normalize nodelta
1274	whd in match (eval_unop ????);
1275	cases esg normalize nodelta
1276	whd in match (opt_to_res ???); whd in match (m_bind ?????);
1277	[ %{(sign_ext sz' cm_val')} \| %{(zero_ext sz' cm_val')} ] @conj try @refl
1278	whd in match (eq_rect_r ??????);
1279	-Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
1280	(* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
1281	this reason. *)
1282	lapply Hvalue_eq -Hvalue_eq lapply vi -vi
1283	cases esz normalize nodelta
1284	#vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
1285	whd in match (sign_ext ??); whd in match (zero_ext ??);
1286	%2
1287	]
1288	\| *:
1289	lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1290	* #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr
1291	%{cm_val'} @conj try @refl
1292	lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
1293	-Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
1294	cases cm_val
1295	[ \| #vsz #vi \| \| #vp
1296	\| \| #vsz #vi \| \| #vp
1297	\| \| #vsz #vi \| \| #vp
1298	\| \| #vsz #vi \| \| #vp ]
1299	#Hexec_cm #Hvalue_eq #Hexec_cast
1300	whd in Hexec_cast:(??%%);
1301	[ 1,5,9,13: destruct (Hexec_cast) ]
1302	[ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
1303	lapply Hexec_cast -Hexec_cast
1304	normalize cases (eq_v ?????) normalize
1305	#Habsurd destruct (Habsurd)
1306	]
1307	\| 9: (* Econdition *)
1308	#ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
1309	#cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
1310	#Hexec_cm
1311	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1312	* #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
1313	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1314	#bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
1315	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1316	* #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
1317	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1318	cases (bind_inversion ????? Htranslate) -Htranslate
1319	* #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1320	cases (bind_inversion ????? Htranslate) -Htranslate
1321	* #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
1322	cases (bind_inversion ????? Htranslate) -Htranslate
1323	* #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
1324	lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) -Htypecheck
1325	* #Htypeof_e2_eq_ty
1326	lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1327	lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
1328	>Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2
1329	#Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1330	#Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
1331	cases (bind_inversion ????? Htranslate) -Htranslate
1332	* #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate
1333	cases (bind_inversion ????? Htranslate) -Htranslate
1334	* #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
1335	lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) -Htypecheck
1336	* #Htypeof_e3_eq_ty
1337	lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
1338	lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
1339	>Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
1340	#Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1341	#Hcmexpr_eq3 destruct (Hcm_expr_eq2)
1342	lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1
1343	lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
1344	lapply Hexec_bool_of_val -Hexec_bool_of_val
1345	cases (typeof e1) normalize nodelta
1346	[ \| #esz #esg \| #eptr_ty \| #earray_ty #earray_sz \| #edomain #ecodomain
1347	\| #estructname #efieldspec \| #eunionname #efieldspec \| #eid ]
1348	#Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
1349	whd in Heq:(???%); destruct (Heq)
1350	whd in match (eval_expr ???????);
1351	whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
1352	lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
1353	>Heval_e1 normalize nodelta
1354	lapply Hcm_ifthenelse -Hcm_ifthenelse
1355	lapply Hexec_cond -Hexec_cond
1356	lapply Hexec_bool_of_val -Hexec_bool_of_val
1357	lapply Hvalue_eq1 -Hvalue_eq1
1358	cases cm_cond_val
1359	[ \| #vsz #vi \| \| #vp
1360	\| \| #vsz #vi \| \| #vp
1361	\| \| #vsz #vi \| \| #vp
1362	\| \| #vsz #vi \| \| #vp ]
1363	whd in ⊢ (? → (??%%) → ?);
1364	[ 6:
1365	\| *: #_ #Habsurd destruct (Habsurd) ]
1366	#Hvalue_eq1 #Hsz_check
1367	lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1368	* #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1369	#Heq destruct (Heq)
1370	#Hexec_expr_e1
1371	@(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
1372	return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
1373	with
1374	[ true ⇒ λHeq. ?
1375	\| false ⇒ λHeq. ?
1376	] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
1377	normalize nodelta
1378	>(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
1379	whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
1380	>Heq normalize nodelta
1381	[ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
1382	cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
1383	normalize %{cm_val3} @conj try @refl assumption
1384	\| -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
1385	cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
1386	normalize %{cm_val2} @conj try @refl assumption ]
1387	\| 10: (* andbool *)
1388	#ty cases ty
1389	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1390	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1391	#e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
1392	#cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
1393	(* decompose first slice of clight execution *)
1394	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1395	* #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
1396	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1397	#b * #Hexec_bool_of_val #Hexec_expr
1398	(* decompose translation to Cminor *)
1399	cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
1400	* #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1401	cases (bind_inversion ????? Htranslate) -Htranslate
1402	* #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
1403	[ 2: \| *: #Heq destruct (Heq) ]
1404	(* discriminate I16 and I8 cases *)
1405	(* lapply Hyp_present -Hyp_present
1406	lapply Hexpr_vars -Hexpr_vars
1407	lapply cm_expr -cm_expr cases sz
1408	#cm_expr #Hexpr_vars #Hyp_present normalize nodelta
1409	[ 1,2: #Habsurd destruct (Habsurd) ] *)
1410	(* go on with decomposition *)
1411	#Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
1412	* #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
1413	(* cleanup the type coercion *)
1414	lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
1415	* #Htypeof_e2_eq_ty
1416	lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1417	lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
1418	lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
1419	lapply Hexpr_vars_e2 -Hexpr_vars_e2
1420	lapply cm_expr_e2 -cm_expr_e2
1421	lapply Hexec_expr -Hexec_expr
1422	>Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
1423	#Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
1424	#Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
1425	(* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
1426	* to proceed in decomposing translation. *)
1427	lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
1428	lapply Hexpr_vars_e1 -Hexpr_vars_e1
1429	lapply cm_expr_e1 -cm_expr_e1
1430	lapply Hexec_bool_of_val -Hexec_bool_of_val
1431	cases (typeof e1)
1432	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
1433	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ]
1434	#Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
1435	normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1436	(* translation decomposition terminated. Reduce goal *)
1437	whd in match (eval_expr ???????);
1438	(* We need Hind1. *)
1439	cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
1440	lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
1441	normalize nodelta
1442	(* peform case analysis to further reduce the goal. *)
1443	lapply Hvalue_eq -Hvalue_eq
1444	lapply Hexec_bool_of_val -Hexec_bool_of_val
1445	whd in match (proj2 ???);
1446	cases cl_val_e1
1447	[ \| #vsz #vi \| \| #vp
1448	\| \| #vsz #vi \| \| #vp
1449	\| \| #vsz #vi \| \| #vp
1450	\| \| #vsz #vi \| \| #vp ]
1451	whd in ⊢ ((??%%) → ?);
1452	[ 6:
1453	\| *: #Heq destruct (Heq) ]
1454	#Hsz_check #Hvalue_eq
1455	lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1456	* #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1457	(* preparing case analysis on b *)
1458	lapply Hexec_expr -Hexec_expr
1459	cases b normalize nodelta
1460	[ 2: (* early exit *)
1461	#Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
1462	#Heq_outcome destruct (Heq_outcome) -Heq_outcome
1463	>(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
1464	<e0 whd in match (m_bind ?????);
1465	@cthulhu
1466	(* Pb: incompatible semantics for cl and cm.
1467	* in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
1468	first operand is false (for andbool)
1469	. solution 1 : change semantics to return actual value instead of Vfalse
1470	. solution 2 : change toCminor to introduce another test in the program,
1471	returning Vfalse in case of failure instead of actual value
1472	*) ]
1473	#Hexec_expr #Heq_outcome
1474	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1475	* #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
1476	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1477	#outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
1478	#Heq destruct (Heq)
1479	>(value_eq_int_inversion … Hvalue_eq)
1480	whd in match (eval_bool_of_val ?);
1481	destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
1482	normalize nodelta
1483	cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
1484	>Heval_expr normalize nodelta
1485	%{cm_val_e2} @conj try @refl
1486	whd in Hexec_bool_outcome:(??%%);
1487	normalize nodelta in Hexec_bool_outcome:(??%%);
1488	lapply Hvalue_eq2 -Hvalue_eq2
1489	-Heval_expr
1490	lapply Hexec_bool_outcome -Hexec_bool_outcome
1491	cases cl_val_e2
1492	[ \| #vsz2 #vi2 \| \| #vp2 ] normalize nodelta
1493	#Heq destruct (Heq)
1494	cases (intsize_eq_elim_inversion ??????? Heq)
1495	#Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1496	cases outcome_bool normalize nodelta
1497	(* Problem. cf prev case. *)
1498	@cthulhu
1499	\| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
1500	\| 12: (* sizeof *)
1501	#ty cases ty
1502	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1503	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1504	#ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1505	whd in Hexec_expr:(??%?); destruct (Hexec_expr)
1506	normalize in match (typ_of_type ?);
1507	whd in Htranslate:(??%?); destruct (Htranslate)
1508	whd in match (eval_expr ???????);
1509	%{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
1510	\| 13:
1511	#ty #ed #ty' cases ty'
1512	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1513	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1514	#i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
1515	#Hexec_lvalue
1516	whd in Hexec_lvalue:(??%?); destruct
1517	[ whd in Htranslate_addr:(??%?);
1518	cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1519	* #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
1520	cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1521	#field_off * #Hfield_off whd in ⊢ ((???%) → ?);
1522	#Heq destruct (Heq)
1523	cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
1524	]
1525	cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1526	* * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue
1527	[ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
1528	#Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
1529	cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
1530	#cm_val_field * #Heval_cm #Hvalue_eq
1531	whd in match (eval_expr ???????);
1532	>Heval_cm normalize nodelta
1533	whd in match (eval_expr ???????); whd in match (m_bind ?????);
1534	whd in match (eval_binop ???????); normalize nodelta
1535	cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
1536	normalize nodelta #Hptr_translate
1537	%{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
1538	@conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
1539	%4 whd in Hptr_translate:(??%?) ⊢ (??%?);
1540	cases (E cl_blo) in Hptr_translate; normalize nodelta
1541	[ #H destruct (H) ]
1542	* #BL #OFF normalize nodelta #Heq destruct (Heq)
1543	>Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
1544	#H destruct (H)
1545	(* again, mismatch in the size of the integers *)
1546	@cthulhu
1547	\| 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
1548	cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
1549	#cm_val * #Heval_expr >Heval_expr #Hvalue_eq
1550	cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
1551	#Hpointer_translation
1552	%{cm_val} @conj try assumption
1553	destruct @refl
1554	]
1555	\| 14: (* cost label *)
1556	#ty (* cases ty
1557	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1558	\| #structname #fieldspec \| #unionname #fieldspec \| #id ] *)
1559	#l * #ed #ety
1560	whd in match (typeof ?); whd in match (typeof ?);
1561	#Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1562	cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
1563	#Hexpr_vars * #Htranslate_ind #Htranslate
1564	cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
1565	* whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
1566	whd in match (typeof ?) in Htyp_should_eq:(??%?);
1567	lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
1568	#Htyp_eq
1569	lapply Htyp_should_eq -Htyp_should_eq
1570	lapply Htranslate_ind -Htranslate_ind
1571	lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
1572	lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
1573	lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1574	lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
1575	<(Htyp_eq)
1576	#cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
1577	#Htranslate_ind
1578	whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta
1579	whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????);
1580	cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
1581	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1582	cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
1583	#cm_val' * #Heval_expr' #Hvalue_eq
1584	>Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
1585	(* Inconsistency in clight and cminor executable semantics for expressions~:
1586	placement of the label is either before or after current trace.
1587	To be resolved.
1588	*)
1589	@cthulhu
1590	\| 15: *
1591	[ #sz #i \| #var_id \| #e1 \| #e1 \| #op #e1 \| #op #e1 #e2 \| #cast_ty #e1
1592	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
1593	#ty normalize in ⊢ (% → ?);
1594	[ 2,3,12: @False_ind
1595	\| *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
1596	normalize #Habsurd destruct (Habsurd) ]
1597	] qed.
1598
1599
1600	axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
1601
1602	(* Conjectured simulation results
1603
1604	We split these based on the start state:
1605
1606	1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
1607	normal steps in Cminor;
1608	2. call and return steps are simulated by a call/return step plus [m] normal
1609	steps (to copy stack allocated parameters / results); and
1610	3. lone cost label steps are simulates by a lone cost label step
1611
1612	These should allow us to maintain enough structure to identify the Cminor
1613	subtrace corresponding to a measurable Clight subtrace.
1614	*)
1615
1616	definition clight_normal : Clight_state → bool ≝
1617	λs. match Clight_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
1618
1619	definition cminor_normal : Cminor_state → bool ≝
1620	λs. match Cminor_classify s with [ cl_other ⇒ true \| cl_jump ⇒ true \| _ ⇒ false ].
1621
1622	axiom clight_cminor_normal :
1623	∀INV:clight_cminor_inv.
1624	∀s1,s1',s2,tr.
1625	clight_cminor_rel INV s1 s1' →
1626	clight_normal s1 →
1627	¬ Clight_labelled s1 →
1628	∃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〉) →
1629	∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1630	tr = tr' ∧
1631	clight_cminor_rel INV s2 s2'
1632	).
1633
1634	axiom clight_cminor_call_return :
1635	∀INV:clight_cminor_inv.
1636	∀s1,s1',s2,tr.
1637	clight_cminor_rel INV s1 s1' →
1638	match Clight_classify s1 with [ cl_call ⇒ true \| cl_return ⇒ true \| _ ⇒ false ] →
1639	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1640	∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1641	tr = tr' ∧
1642	clight_cminor_rel INV s2 s2'
1643	).
1644
1645	axiom clight_cminor_cost :
1646	∀INV:clight_cminor_inv.
1647	∀s1,s1',s2,tr.
1648	clight_cminor_rel INV s1 s1' →
1649	Clight_labelled s1 →
1650	after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1651	after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
1652	tr = tr' ∧
1653	clight_cminor_rel INV s2 s2'
1654	).
1655

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

Download in other formats:

Original Format