source: src/Clight/toCminorCorrectness.ma @ 2588

Last change on this file since 2588 was 2588, checked in by garnier, 7 years ago

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File size: 120.1 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/toCminorOps.ma".
3include "Clight/CexecInd.ma".
4include "common/Globalenvs.ma".
5include "Clight/memoryInjections.ma".
6include "Clight/abstract.ma".
7include "Cminor/abstract.ma".
8
9
10(* When we characterise the local Clight variables, those that are stack
11   allocated are given disjoint regions of the stack. *)
12
13lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
14  characterise_vars globals f = 〈vartypes, stacksize〉 →
15  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
16  ∀id',n',ty'. id ≠ id' →
17  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
18  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
19#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
20whd in ⊢ (??%? → ?);
21generalize in match vartypes; -vartypes
22generalize in match stacksize; -stacksize
23elim (args@vars)
24[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
25  elim globals in L;
26  [ normalize #L destruct
27  | * * #id' #r #ty' #tl #IH
28    whd in match (foldr ?????);
29    #L cases (lookup_add_cases ??????? L)
30    [ * #E1 #E2 destruct
31    | @IH
32    ]
33  ]
34| * #id1 #ty1 #tl #IH #stacksize #vartypes
35  whd in match (foldr ?????);
36  (* Avoid writing out the definition again *)
37  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
38  lapply (refl ? ih) whd in match ih; -ih
39  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
40  #vartypes' #stack' #FOLD #IH
41  whd in ⊢ (??(match % with [_⇒?])? → ?);
42  cases (orb ??)
43  #CHAR whd in CHAR:(??%?); destruct
44  #L cases (lookup_add_cases ??????? L)
45  [ 1,3: * #E1 #E2 destruct
46    #id' #n' #ty' #NE >lookup_add_miss /2/
47    #L' %1 -L -IH
48    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
49    generalize in match stack'; -stack'
50    elim tl
51    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
52      elim globals in L';
53      [ normalize #E destruct
54      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
55        #L cases (lookup_add_cases ??????? L)
56        [ * #E1 #E2 destruct
57        | @IH
58        ]
59      ]
60    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
61      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
62      #vartypes2 #stack2 #IH
63      whd in ⊢ (??%? → ?);
64      cases (orb ??)
65      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
66        [ * #E1 #E2 destruct //
67        | #L'' lapply (IH ?? (refl ??) L'') /2/
68        ]
69      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
70        [ * #E1 #E2 destruct
71        | #L'' lapply (IH ?? (refl ??) L'') /2/
72        ]
73      ]
74    ]
75  | -L #L #id' #n' #ty' #NE #L'
76    cases (lookup_add_cases ??????? L')
77    [ * #E1 #E2 destruct
78      %2 -IH -L'
79      generalize in match vartypes' in FOLD L; -vartypes'
80      generalize in match stack'; -stack'
81      elim tl
82      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
83        elim globals in L;
84        [ normalize #E destruct
85        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
86          #L cases (lookup_add_cases ??????? L)
87          [ * #E1 #E2 destruct
88          | @IH
89          ]
90        ]
91      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
92        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
93        #vartypes2 #stack2 #IH
94        whd in ⊢ (??%? → ?);
95        cases (orb ??)
96        #E whd in E:(??%?); destruct
97        #L cases (lookup_add_cases ??????? L)
98        [ 1,3: * #E1 #E2 destruct //
99        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
100        ]
101      ]
102    | @(IH … (refl ??) L … NE)
103    ]
104  | -L #L #id' #n' #ty' #NE #L'
105    cases (lookup_add_cases ??????? L')
106    [ * #E1 #E2 destruct
107    | @(IH … (refl ??) L … NE)
108    ]
109  ]
110] qed.
111
112(* And everything is in the stack frame. *)
113
114lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
115  characterise_vars globals f = 〈vartypes, stacksize〉 →
116  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
117  n + sizeof ty ≤ stacksize.
118#globals * #ret #args #vars #body whd in match (characterise_vars ??);
119elim (args@vars)
120[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
121  whd in FOLD:(??%?); destruct elim globals in L;
122  [ #E normalize in E; destruct
123  | * * #id' #r' #ty' #tl' #IH
124    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
125    [ * #E1 #E2 destruct
126    | @IH
127    ]
128  ]
129| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
130  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
131  #vartypes' #stackspace' #IH
132  whd in ⊢ (??(match % with [_⇒?])? → ?);
133  cases (orb ??) whd in ⊢ (??%? → ?);
134  #E destruct #L cases (lookup_add_cases ??????? L)
135  [ 1,3: * #E1 #E2 destruct //
136  | 2,4: #L' lapply (IH … (refl ??) L') /2/
137  ]
138] qed.
139
140(* Local variables show up in the variable characterisation as local. *)
141
142lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
143  characterise_vars globals f = 〈vartypes, stacksize〉 →
144  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
145  ∃t. local_id vartypes id t.
146#globals * #ret #args #vars #body
147whd in match (characterise_vars ??); elim (args@vars)
148[ #vartypes #stacksize #id #_ *
149| * #hd #ty #tl #IH
150  #vartypes #stacksize #id
151  whd in match (foldr ?????);
152  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
153  #vartypes' #stackspace' #IH
154  whd in ⊢ (??(match % with [_⇒?])? → ?);
155  cases (orb ??)
156  #E whd in E:(??%?); destruct *
157  [ 1,3: #E destruct %{(typ_of_type ty)}
158    whd whd in match (lookup' ??); >lookup_add_hit //
159  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
160    cases (identifier_eq ? id hd)
161    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
162    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
163    ]
164  ]
165] qed.
166
167(* Put knowledge that Globals are global into a more useful form than the
168   one used for the invariant. *)
169
170lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
171  characterise_vars globals f = 〈vartypes, stacksize〉 →
172  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
173  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
174  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
175#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
176cases (characterise_vars_src … CHAR id ?)
177[ * #r' * #ty' >L
178  * #E1 destruct (E1) #EX
179  %
180  [ @EX
181  | % #EX' cases (characterise_vars_localid … CHAR EX')
182    #ty' whd in ⊢ (% → ?); >L *
183  ]
184| * #ty' whd in ⊢ (% → ?); >L *
185| whd >(opt_eq_from_res ???? L) % #E destruct
186] qed.
187
188
189(* Show how the global environments match up. *)
190
191lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
192  map_partial_All A B P f l H = OK ? l' →
193  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
194#A #B #P #f #l
195elim l
196[ #H #l' #MAP normalize in MAP; destruct //
197| #h #t #IH * #p #H #l'
198  whd in ⊢ (??%? → ?);
199  lapply (refl ? (f h p)) whd in match (proj1 ???);
200  cases (f h p) in ⊢ (???% → %);
201  [ #b #E #MAP cases (bind_inversion ????? MAP)
202    #tl' * #MAP' #E' normalize in E'; destruct
203    % [ %{p} @E | @IH [ @H | @MAP' ] ]
204  | #m #_ #X normalize in X; destruct
205  ]
206] qed.
207 
208
209definition clight_cminor_matching : clight_program → matching ≝
210λp.
211  let tmpuniverse ≝ universe_for_program p in
212  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
213  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
214  let globals ≝ fun_globals @ var_globals in
215  mk_matching
216    ?? (list init_data × type) (list init_data)
217    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
218    (λv,w. \fst v = w).
219
220lemma clight_to_cminor_varnames : ∀p,p'.
221  clight_to_cminor p = OK ? p' →
222  prog_var_names … p = prog_var_names … p'.
223* #vars #fns #main * #vars' #fns' #main'
224#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
225whd in E:(??%%); destruct
226-MAP normalize
227elim vars
228[ //
229| * * #id #r * #d #t #tl #IH normalize >IH //
230] qed.
231
232
233lemma clight_to_cminor_matches : ∀p,p'.
234  clight_to_cminor p = OK ? p' →
235  match_program (clight_cminor_matching p) p p'.
236* #vars #fns #main * #vars' #fns' #main'
237#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
238whd in E:(??%%); destruct
239%
240[ -MAP whd in match (m_V ?); whd in match (m_W ?);
241  elim vars
242  [ //
243  | * * #id #r * #init #ty #tl #IH %
244    [ % //
245    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
246    ]
247  ]
248| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
249  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
250  normalize in E; destruct
251  <(clight_to_cminor_varnames … TO)
252  % whd
253  % [2: % [2: @TRANSF | skip ] | skip ]
254| %
255] qed.
256
257(* Invariants used in simulation *)
258
259record clight_cminor_inv : Type[0] ≝ {
260  globals : list (ident × region × type);
261  ge_cl : genv_t clight_fundef;
262  ge_cm : genv_t (fundef internal_function);
263  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
264  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
265    ∃tmp_u,f',H1,H2.
266      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
267      find_funct … ge_cm v = Some ? f'
268}.
269
270(* Perhaps we will have to be more precise on what is allocated, etc.
271   cf [exec_alloc_variables]. For now this is conveniently hidden in
272   the [value_eq E v v'] *)
273definition memory_matching ≝
274  λE:embedding.
275  λm,m':mem.
276  λen:cl_env.
277  λvenv:cm_env.
278  λcminv:clight_cminor_inv.
279  λsp:block.
280  λvars:var_types.
281  ∀id.
282    match lookup SymbolTag ? en id with
283    [ None ⇒
284      match find_symbol ? (ge_cl cminv) id with
285      [ None ⇒ True
286      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
287      ]
288    | Some cl_blo ⇒
289         match lookup ?? vars id with
290         [ Some kind ⇒
291            let 〈vtype, type〉 ≝ kind in
292            match vtype with
293            [ Stack n ⇒
294              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
295            | Local ⇒
296              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
297                   ∃v'. lookup ?? venv id = Some ? v' ∧
298                        value_eq E v v'
299            | _ ⇒ False ]
300        | None ⇒ False ]
301    ].
302
303lemma load_value_of_type_by_ref :
304  ∀ty,m,b,off,val.
305    load_value_of_type ty m b off = Some ? val →
306    typ_of_type ty ≃ ASTptr →
307    access_mode ty ≃ By_reference →
308    val = Vptr (mk_pointer b off).
309*
310[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
311| #structname #fieldspec | #unionname #fieldspec | #id ]
312#m #b #off #val
313[ 1,6,7: normalize #Habsurd destruct (Habsurd)
314| 4,5: normalize #Heq #_ #_ destruct @refl
315| 2: #_ normalize #Heq destruct
316| *: #Hload normalize #_ #H
317      lapply (jmeq_to_eq ??? H) #Heq destruct
318] qed.
319
320lemma load_value_of_type_by_value :
321  ∀ty,m,b,off,val.
322  access_mode ty = By_value (typ_of_type ty) →
323  load_value_of_type ty m b off = Some ? val →
324  loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
325
326[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
327| #structname #fieldspec | #unionname #fieldspec | #id ]
328#m #b #off #val
329normalize in match (access_mode ?);
330[ 1,4,5,6,7: #Habsurd destruct ]
331#_
332#H @H
333qed.
334
335lemma lookup_exec_alloc :
336  ∀source_variables, initial_env, env, var_id, clb, m, m'.
337  lookup ?? env var_id = Some ? clb →
338  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
339  lookup ?? initial_env var_id = Some ? clb ∨
340  Exists ? (λx. \fst x = var_id) source_variables.
341#source_variables
342elim source_variables
343[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
344     destruct (Hexec_alloc) %1 @Hlookup
345| 2: * #id #ty #tail #Hind
346     #init_env #env #var #clb #m #m' #Hlookup     
347     whd in ⊢ (??%? → ?);
348     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
349     #Hexec_alloc
350     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
351     [ 1: destruct (Heq) %2 %1 @refl ]
352     cases (Hind … Hlookup Hexec_alloc)
353     [ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup
354     | #Hexists %2 %2 @Hexists ]
355] qed.
356
357lemma characterise_vars_lookup_local :
358  ∀globals,f,vartypes,stacksize,id,clb,env.
359   characterise_vars globals f = 〈vartypes, stacksize〉 →
360   lookup ?? env id = Some ? clb →
361   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
362   ∃t. local_id vartypes id t.
363#globals #f #vartypes #stacksize #id #clb #env
364#Hchar #Hlookup * #m * #m' #Hexec
365cases (lookup_exec_alloc … Hlookup Hexec)
366[ normalize in ⊢ (% → ?); #Heq destruct
367| @(characterise_vars_localid … Hchar) ]
368qed.
369
370
371lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
372  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
373  lookup ?? env' var_id = None ? →
374  lookup ?? env var_id = None ? ∧
375  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
376#vars elim vars
377[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
378  #H @conj try @H % //
379| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
380  whd in ⊢ ((??%?) → ? → ?);
381  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
382  normalize nodelta #Hexec #Hlookup
383  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
384  cases env #env cases id' #id' cases var #var normalize
385  @(eqb_elim … id' var)
386  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
387       #Heq <Heq @conj try @Hlookup' % *
388       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
389       | cases Hexists' #H @H ]
390  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
391       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
392       >H1 in Hlookup'; #Heq destruct
393  ]
394] qed.
395
396lemma variable_not_in_env_but_in_vartypes_is_global :
397  ∀env,env',f,vars,stacksize,globals,var_id.
398  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
399  characterise_vars globals f =〈vars,stacksize〉 →
400  lookup ?? env' var_id = None ? →       
401  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
402  ∃r.allocty = Global r.
403#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
404#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
405lapply (characterise_vars_src … Hcharacterise var_id ?)
406[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
407 #Hlookup >Hlookup #_ #Habsurd destruct ]
408*
409[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
410     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
411* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
412@(match allocty
413  return λx. allocty = x → ?
414  with
415  [ Global r ⇒ λ_. ?
416  | Stack st' ⇒ λHalloc. ?
417  | Local ⇒ λHalloc. ?
418  ] (refl ? allocty))
419[ @False_ind ] normalize nodelta
420#Heq_typ
421(* Halloc is in contradiction with Hlookup_fail *)
422lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
423* #Hlookup' #Hnot_exists
424lapply (characterise_vars_all … Hcharacterise var_id t ?)
425[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
426#Hexists @False_ind
427cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
428[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
429       * #id' #ty' #tl #Hind *
430       [ 1,3: * #Heq #_ %1 @Heq
431       | *: #H %2 @Hind @H ] ]
432#H cases Hnot_exists #H' @H' @H
433qed.
434
435(* avoid a case analysis on type inside of a big proof *)
436lemma match_type_inversion_aux : ∀ty,e,f.
437 match ty in type return λty':type.(res (expr (typ_of_type ty'))) with 
438  [Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
439  |Tint (sz:intsize)   (sg:signedness)⇒ f sz sg
440  |Tpointer (x:type)⇒
441   Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch)
442  |Tarray (x:type)   (y:ℕ)⇒
443   Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch)
444  |Tfunction (x:typelist)   (y:type)⇒
445   Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch)
446  |Tstruct (x:ident)   (y:fieldlist)⇒
447   Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
448  |Tunion (x:ident)   (y:fieldlist)⇒
449   Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
450  |Tcomp_ptr (x:ident)⇒
451   Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)]
452  = OK ? e →
453  ∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e).
454*
455[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
456| #structname #fieldspec | #unionname #fieldspec | #id ]
457whd in match (typ_of_type Tvoid);
458#e #f normalize nodelta #Heq destruct
459%{sz} %{sg} % try @refl >Heq %
460qed.
461
462
463(* The two following lemmas are just noise. *)
464
465lemma expr_vars_fix_ptr_type :
466  ∀ty',optlen.
467  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
468  ∀P.
469   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
470   expr_vars
471    (typ_of_type
472        match optlen 
473        in option 
474        return λ_:(option ℕ).type with 
475        [None⇒Tpointer ty'
476        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
477#ty' * normalize
478[ 2: #n ]
479#e #P
480@expr_vars_mp //
481qed.
482
483lemma eval_expr_rewrite_aux :
484  ∀genv.
485  ∀optlen.
486  ∀ty'.
487  ∀e.
488  ∀cm_env.
489  ∀H.
490  ∀sp.
491  ∀m.
492  ∀res.
493  (eval_expr genv
494             (typ_of_type
495                 match optlen in option return λ_:(option ℕ).type with 
496                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
497             e cm_env (expr_vars_fix_ptr_type ty' optlen e (λid:ident.λty0:typ.present SymbolTag val cm_env id) H) sp m) = OK ? res →
498   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
499#genv * [ 2: #n ] normalize nodelta
500#ty' normalize in match (typ_of_type ?);
501#e #cm_env whd in match (fix_ptr_type ???);
502#H #sp #m #res #H @H
503qed.
504
505lemma sign_ext_sign_ext_reduce :
506  ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
507#i @refl
508qed. 
509
510lemma sign_ext_zero_ext_reduce :
511  ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
512#i @refl
513qed.
514
515(* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
516 * the cleanup ourselves. *)
517
518definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
519definition zero_ext_val : ∀target_sz:intsize. val → val ≝ zero_ext.
520
521(* CM code uses 8 bit constants and upcasts them to target_size, CL uses 32 bit and
522 * downcasts them to target_size. In the end, these are equal. We directly state what
523 * we need. *)
524lemma value_eq_cl_cm_true :
525  ∀E,sz.
526  value_eq E
527    (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 1)))
528    (zero_ext_val sz (Vint I8 (repr I8 1))).
529#E * %2 qed.
530
531lemma value_eq_cl_cm_false :
532  ∀E,sz.
533  value_eq E
534    (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 0)))
535    (zero_ext_val sz (Vint I8 (repr I8 0))).
536#E * %2 qed.
537
538lemma exec_bool_of_val_inversion : ∀v,ty,b.
539  exec_bool_of_val v ty = OK ? b →
540  (∃sz,sg,i. v = Vint sz i ∧ ty = Tint sz sg ∧ b = (¬eq_bv (bitsize_of_intsize sz) i (zero (bitsize_of_intsize sz)))) ∨
541  (∃ty'. v = Vnull ∧ ty = Tpointer ty' ∧ b = false) ∨
542  (∃ptr,ty'. v = Vptr ptr ∧ ty = Tpointer ty' ∧ b = true).
543#v #ty #b #Hexec
544cases v in Hexec;
545[ | #vsz #i | | #p ]
546cases ty
547[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
548| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
549| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
550| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
551whd in ⊢ ((??%%) → ?);
552#Heq destruct (Heq)
553[ 2: %1 %2 %{ptr_ty} @conj try @conj try @refl
554| 3: %2 %{p} %{ptr_ty}  @conj try @conj try @refl
555| 1: %1 %1 %{sz} %{sg} lapply Heq -Heq
556     cases vsz in i; #i cases sz whd in ⊢ ((??%?) → ?);
557     #Heq destruct %{i} @conj try @conj try @refl
558] qed.     
559
560(* This lemma is noise I extracted from the proof below, even though it is used only once.
561   Better that than an ugly cut.
562   We need the following lemma to feed another one down in the deref case. In essence,
563   it says that the variables present in a cminor expression resulting from converting
564   a clight deref are transmitted to the cminor counterpart of the pointer argument.
565   This is made messy by the fact that clight to cminor implements different deref
566   strategies for different kind of variables.   
567*)
568lemma translate_expr_deref_present:
569      ∀vars:var_types.
570      ∀ptrdesc:expr_descr.
571      ∀ptrty:type.
572      ∀derefty:type.
573      ∀cm_deref.
574      ∀Hcm_deref.
575      ∀cm_ptr.
576      ∀Hcm_ptr.
577      ∀cm_env:env.
578        translate_expr vars (Expr (Ederef (Expr ptrdesc ptrty)) derefty) =OK ? «cm_deref,Hcm_deref» →
579        expr_vars (typ_of_type derefty) cm_deref (λid:ident.λty0:typ.present SymbolTag ? cm_env id) →
580        translate_expr vars (Expr ptrdesc ptrty) =OK ? «cm_ptr,Hcm_ptr» →
581        expr_vars ? cm_ptr (λid:ident.λty0:typ.present SymbolTag ? cm_env id).
582  #cut_vars #ptrdesc #ptrty #derefty
583  cases ptrty
584  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
585  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
586  #cut_cm_deref #Hcut_cm_deref #cut_cm_ptr #Hcut_cm_ptr #cut_cm_env
587  whd in match (translate_expr ??);
588  cases (translate_expr cut_vars (Expr ptrdesc ?)) normalize nodelta
589  [ 1,2,3,4,6,8,10,11,12,13,14,16: #err #Habsurd destruct (Habsurd) ]
590  normalize in match (typ_of_type ?);
591  * #cut_e' #Hcut_local_e'
592  lapply Hcut_cm_deref -Hcut_cm_deref lapply cut_cm_deref -cut_cm_deref
593  cases (access_mode derefty) normalize nodelta
594  [ #invert_ty | | #invert_ty
595  | #invert_ty | | #invert_ty
596  | #invert_ty | | #invert_ty
597  | #invert_ty | | #invert_ty ]
598  [ 3,6,9,12: #cut_cm_deref #Hcut_cm_deref #Habsurd destruct (Habsurd) ]
599  #cut_cm_deref #Hcut_cm_deref #Heq destruct (Heq)
600  [ 1,3,5,7: whd in ⊢ (% → ?); ]
601  #Hgoal #Heq destruct @Hgoal
602qed.
603
604(* TODOs : there are some glitches between clight and cminor :
605 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
606      in the shortcut case, the cminor code returns directly the outcome of the
607      evaluated expr, with a possibly different size.
608   2) another glitch is for the integer/pointer additions: Clight always performs
609      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
610      the sign of i, producing either a sign extension or a zero extension.
611   3) something similar to 1) happens for binary comparison operators. Clight generates
612      systematically a 32 bit value for the outcome of the comparison and lives with it,
613      but toCminor actually generates something 8 bit and casts it back to the context type.
614   4) we need some proof that we don't blow the stack during the transformation. Otherwise,
615      a problem appears when we prove semantics preservation for pointer < comparison
616      (we might wrap up the rhs and end SNAFU).
617 *)
618 
619lemma eval_expr_sim :
620  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
621  ∀cl_cm_inv  : clight_cminor_inv.
622  (* current function (defines local environment) *)
623  ∀f          : function.
624  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
625  ∀alloctype  : var_types.
626  ∀stacksize  : ℕ.
627  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
628  (* environments *)
629  ∀cl_env     : cl_env.
630  ∀cm_env     : cm_env.
631  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
632  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
633  (* CL and CM memories *)
634  ∀cl_m       : mem.
635  ∀cm_m       : mem.
636  (* memory injection and matching *)
637  ∀embed      : embedding.
638  ∀injection  : memory_inj embed cl_m cm_m.
639  ∀stackptr   : block.
640  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
641  (* clight expr to cminor expr *)
642  (∀(e:expr).
643   ∀(e':CMexpr (typ_of_type (typeof e))).
644   ∀Hexpr_vars.
645   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
646   ∀cl_val,trace,Hyp_present.
647   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
648   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
649            value_eq embed cl_val cm_val) ∧
650   (* clight /lvalue/ to cminor /expr/ *)
651  (∀ed,ty.
652   ∀(e':CMexpr ASTptr).
653   ∀Hexpr_vars.
654   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
655   ∀cl_blo,cl_off,trace,Hyp_present.
656   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
657   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
658            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
659#inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
660@expr_lvalue_ind_combined
661[ 7: (* binary ops *)
662     #ty
663     #op #e1 #e2
664     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
665     cases (bind_inversion ????? Htranslate) -Htranslate
666     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
667     cases (bind_inversion ????? Htranslate) -Htranslate
668     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
669     whd in ⊢ ((??%?) → ?);
670     #Htranslate_binop
671     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
672     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
673     #cl_val #trace #Hyp_present #Hexec
674     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
675     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
676     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
677     lapply Hyp_present -Hyp_present
678     lapply Htranslate_lhs -Htranslate_lhs
679     lapply Htranslate_rhs -Htranslate_rhs
680     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
681     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
682     lapply Hexec -Hexec
683     lapply Htranslated_binop -Htranslated_binop
684     lapply rhs -rhs lapply lhs -lhs
685     (* end of dump *)
686     cases op
687     whd in ⊢ (? → ? → (??%?) → ?);
688     [ 1: (* add *)
689       lapply (classify_add_inversion (typeof e1) (typeof e2))
690       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
691       (* trying to factorise as much stuff as possible ... *)
692       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
693       * [ 1: * ]
694       [ 1: * #sz * #sg * *
695       | 2: * #optlen * #ty' * #sz * #sg * *
696       | 3: * #optlen * #sz * #sg * #ty' * * ]
697       whd in match (typeof ?) in ⊢ (% → % → ?);
698       #Htypeof_e1 #Htypeof_e2
699       >Htypeof_e1 >Htypeof_e2
700       #Hclassify
701       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
702       normalize nodelta
703       whd in match (typeof ?) in ⊢ (% → % → %);
704       whd in match (typ_of_type (Tint ??));
705       #lhs #rhs #Htyp_should_eq
706       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
707       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
708       -Htyp_should_eq
709       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
710       <Heq_e' -Heq_e'
711       #Hexec
712       #Hexpr_vars_rhs #Hexpr_vars_lhs
713       #Htranslate_rhs #Htranslate_lhs
714       * [ #Hyp_present_lhs #Hyp_present_rhs
715         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
716         | * #Hyp_present_lhs #Hyp_present_cst #Hyp_present_rhs ]
717       whd in match (typeof ?);
718       #Hind_rhs #Hind_lhs
719       cases (bind_inversion ????? Hexec) -Hexec
720       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
721       cases (bind_inversion ????? Hexec) -Hexec
722       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
723       cases (bind_inversion ????? Hexec) -Hexec
724       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
725       lapply (opt_to_res_inversion ???? Hsem) -Hsem
726       whd in match (typeof ?); whd in match (typeof ?);
727       #Hsem_binary
728       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
729       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
730       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
731       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
732       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
733       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
734       whd in match (eval_expr ???????);
735       whd in match (proj1 ???);
736       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
737       [ 1,2: >Heval_lhs normalize nodelta
738              whd in match (eval_expr ???????);
739              whd in match (eval_expr ???????);
740              >Heval_rhs normalize nodelta
741              whd in match (m_bind ?????);
742       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
743            whd in match (eval_expr ???????);
744            whd in match (eval_expr ???????);
745            >Heval_lhs normalize nodelta
746       ]
747       whd in match (proj1 ???); whd in match (proj2 ???);
748       [ 2: (* standard int/int addition. *)
749            whd in match (eval_binop ???????);
750            whd in Hsem_binary:(??%?);
751            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
752            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
753            cases (sem_add_ii_inversion … Hsem_binary_translated)
754            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
755            #Hcm_lhs #Hcm_rhs #Hcm_val
756            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
757            >intsize_eq_elim_true normalize nodelta
758            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
759            @conj try @refl lapply Hsem_binary_translated
760            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
761            >inttyp_eq_elim_true' normalize nodelta
762            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
763       | *: (* pointer/int int/pointer addition *)
764            whd in Hsem_binary:(??%?);
765            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
766            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
767            (* >> *)             
768            [ lapply (sem_add_pi_inversion … Hsem_binary_translated)
769              * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
770              [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
771              | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
772            | lapply (sem_add_ip_inversion … Hsem_binary_translated)
773              * #cm_vsz * #cm_lhs_v * #Hcm_lhs *
774              [ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr
775              | * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ]
776            ]
777            destruct
778            whd in match (eval_unop ????);
779            @(match sg
780              return λs. sg = s → ?
781              with
782              [ Unsigned ⇒ λHsg. ?
783              | Signed ⇒ λHsg. ?
784              ] (refl ??)) normalize nodelta
785            whd in match (eval_binop ???????);
786            whd in match (m_bind ?????);
787            [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
788                            (short_multiplication (bitsize_of_intsize I16)
789                            (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
790                            (repr I16 (sizeof ty')))))}
791            | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
792                          (short_multiplication (bitsize_of_intsize I16)
793                          (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
794                          (repr I16 (sizeof ty')))))}
795            | 5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
796                          (short_multiplication (bitsize_of_intsize I16)
797                          (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
798                          (repr I16 (sizeof ty')))))}
799            | 6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
800                          (short_multiplication (bitsize_of_intsize I16)
801                          (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
802                          (repr I16 (sizeof ty')))))}
803            ]
804            [ 1,2,3,4: @conj whd in match (E0);
805                        whd in match (Eapp trace_rhs ?);
806                        whd in match (Eapp trace_lhs ?);
807                        >(append_nil … trace_rhs) try @refl
808                        >(append_nil … trace_lhs) try @refl
809                        @(value_eq_triangle_diagram … Hvalue_eq_res)
810                        whd in match (shift_pointer_n ?????);
811                        whd in match (shift_offset_n ?????);
812                        >Hsg normalize nodelta
813                        >commutative_short_multiplication
814                        whd in match (shift_pointer ???);
815                        whd in match (shift_offset ???);
816                        >sign_ext_same_size @refl
817           | 5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
818           | 6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]           
819           >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
820           >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
821           normalize >append_nil try @refl
822       ]
823     | 2: (* subtraction cases: not quite identical to add. *)
824       lapply (classify_sub_inversion (typeof e1) (typeof e2))
825       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
826       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
827       * [ 1: * ]
828       [ 1: * #sz * #sg * *
829       | 2: * #optlen * #ty' * #sz * #sg * *
830       | 3: * #t1 * #t2 * #n1 * #n2 * * ]
831       whd in match (typeof ?) in ⊢ (% → % → ?);
832       #Htypeof_e1 #Htypeof_e2
833       >Htypeof_e1 >Htypeof_e2
834       #Hclassify
835       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
836       normalize nodelta
837       whd in match (typeof ?) in ⊢ (% → % → %);
838       whd in match (typ_of_type (Tint ??));
839       #lhs #rhs
840       [ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
841            -Htyp_should_eq
842       | 2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq)
843            -Htyp_should_eq
844       | 3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * -Haux
845            #Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) -Heq_aux
846            #Heq_e' destruct (Heq_e') ]
847       [ 1,2: #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
848              <Heq_e' -Heq_e' | ]
849       #Hexec
850       #Hexpr_vars_rhs #Hexpr_vars_lhs
851       #Htranslate_rhs #Htranslate_lhs
852       * [ #Hyp_present_lhs #Hyp_present_rhs
853         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
854         | * #Hyp_present_lhs #Hyp_present_rhs #Hyp_present_cst ]
855       whd in match (typeof ?);
856       #Hind_rhs #Hind_lhs
857       cases (bind_inversion ????? Hexec) -Hexec
858       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
859       cases (bind_inversion ????? Hexec) -Hexec
860       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
861       cases (bind_inversion ????? Hexec) -Hexec
862       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
863       lapply (opt_to_res_inversion ???? Hsem) -Hsem
864       whd in match (typeof ?); whd in match (typeof ?);
865       #Hsem_binary
866       whd in match (eval_expr ???????);
867       whd in match (proj1 ???);
868       whd in match (eval_expr ???????);
869       whd in match (eval_expr ???????);
870       whd in match (proj1 ???);
871       [ 1: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
872       | 2,3: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
873       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
874       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
875       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
876       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
877       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
878       [ 1,2: >Heval_lhs normalize nodelta
879              whd in match (eval_expr ???????);
880              whd in match (eval_expr ???????);
881              whd in match (proj2 ???);
882              [ >(eval_expr_rewrite_aux … Heval_rhs)
883              | >Heval_rhs ]
884              whd in match (m_bind ?????);
885              normalize nodelta
886       | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
887            whd in match (eval_expr ???????);
888            whd in match (proj2 ???);
889            whd in match (eval_expr ???????);
890            whd in match (proj1 ???);
891            whd in match (eval_expr ???????);
892            >Heval_rhs normalize nodelta
893            whd in match (eval_unop ????);
894       ]
895       [ 1:       
896        (* ptr/ptr sub *)
897            whd in Hsem_binary:(??%?);
898            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
899            -Hsem_binary
900            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
901            lapply (sem_sub_pp_inversion … Hsem_binary_translated)
902            * #ty_sz' * #ty_sg' * #Heq destruct (Heq) *
903            [ (* regular pointers case *)
904              * #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
905              #Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq
906              whd in match (eval_binop ???????);
907              >Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b
908              normalize nodelta
909              whd in match (eval_expr ???????);
910              whd in match (m_bind ?????);
911              whd in match (eval_binop ???????);
912              normalize in match (bitsize_of_intsize ?);
913              normalize in match (S (7+pred_size_intsize I16*8)) in Hoffset_eq;
914              >Hoffset_eq
915              (* whd in match (pred_size_intsize ?); normalize in match (7+1*8); *)
916              (* size mismatch between CL and CM. TODO *)
917              >Hoffset_eq normalize nodelta
918              whd in match (eval_unop ????);
919              %{cm_val} >Hcm_val_eq
920              whd in match (opt_to_res ???);
921              whd in match (m_bind ?????); @conj
922              [ 2: destruct assumption
923              | 1: whd in match (zero_ext ? (Vint ??));
924                   whd in match E0; whd in match (Eapp ? []); >append_nil
925                   normalize in match (bitsize_of_intsize ?); try @refl ]
926            | (* null pointers case *)
927              * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
928              whd in match (eval_binop ???????); normalize nodelta
929              whd in match (eval_expr ???????);
930              whd in match (m_bind ?????);
931              whd in match (eval_binop ???????); normalize nodelta
932              >division_u_zero normalize nodelta
933              whd in match (eval_unop ????);
934              whd in match (opt_to_res ???);
935              whd in match (m_bind ?????);
936              whd in match (pred_size_intsize ?);
937              %{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj
938              [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
939              whd in Hsem_binary_translated:(??%?);
940              normalize nodelta in Hsem_binary_translated:(??%?);
941              lapply Hsem_binary_translated; -Hsem_binary_translated
942              cases n1 cases n2
943              [ | 2,3: #n | #n1 #n2 ] normalize nodelta
944              #Heq destruct (Heq)
945              whd in match (zero_ext ??);
946              cases ty_sz' in Hvalue_eq_res; try //
947            ]
948       | 2: (* int/int sub *)
949            whd in match (eval_binop ???????);
950            whd in Hsem_binary:(??%?);
951            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
952            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
953            cases (sem_sub_ii_inversion … Hsem_binary_translated)
954            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
955            #Hcm_lhs #Hcm_rhs #Hcm_val
956            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
957            >intsize_eq_elim_true normalize nodelta
958            %{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
959            @conj try @refl lapply Hsem_binary_translated
960            whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??);
961            >type_eq_dec_true normalize nodelta
962            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
963       | 3: (* ptr/int sub *)
964            whd in Hsem_binary:(??%?);
965            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary
966            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
967            lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
968            * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
969            [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
970            | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
971            whd in match (eval_unop ????);
972            -Heval_lhs -Heval_rhs destruct
973            whd in match (proj2 ???);
974            whd in match (proj1 ???);
975            whd in match (proj2 ???);           
976            whd in match (eval_expr ???????);
977            @(match sg
978              return λs. sg = s → ?
979              with
980              [ Unsigned ⇒ λHsg. ?
981              | Signed ⇒ λHsg. ?
982              ] (refl ??)) normalize nodelta
983            whd in match (eval_unop ????);
984            whd in match (m_bind ?????);
985            whd in match (eval_binop ???????);
986            [ 1,2:
987               whd in match (neg_shift_pointer_n ?????) in Hvalue_eq_res;
988               whd in match (neg_shift_offset_n ?????) in Hvalue_eq_res;
989               whd in match (neg_shift_pointer ???);
990               whd in match (neg_shift_offset ???);
991               destruct (Hsg) normalize nodelta in Hvalue_eq_res;
992               [ >sign_ext_sign_ext_reduce
993                 %{(Vptr
994                     (mk_pointer (pblock lhs_ptr)
995                      (mk_offset
996                         (subtraction offset_size (offv (poff lhs_ptr))
997                           (short_multiplication (bitsize_of_intsize I16)
998                              (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
999                                 (repr I16 (sizeof ty')))))))}
1000                  @conj
1001                  [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
1002                  | >commutative_short_multiplication @Hvalue_eq_res ]
1003               | >sign_ext_zero_ext_reduce
1004                 %{(Vptr
1005                     (mk_pointer (pblock lhs_ptr)
1006                      (mk_offset
1007                         (subtraction offset_size (offv (poff lhs_ptr))
1008                           (short_multiplication (bitsize_of_intsize I16)
1009                              (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1010                                 (repr I16 (sizeof ty')))))))}
1011                 @conj
1012                  [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
1013                  | >commutative_short_multiplication @Hvalue_eq_res ]
1014              ]                         
1015            ]
1016            [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1017              >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1018              >(sign_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32))
1019            | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1020              >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1021              >(zero_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) ]
1022            >(eq_bv_true … (zero 32)) normalize nodelta
1023           %{Vnull} @conj try assumption
1024           normalize >append_nil try @refl
1025       ]     
1026     | 3: (* mul *)
1027       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1028       [ 2,4: #Hclassify >Hclassify normalize nodelta
1029            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1030       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1031       whd in match (typeof ?); #e'
1032       * #sz * #sg * *
1033       whd in match (typeof ?) in ⊢ (% → % → ?);
1034       #Htypeof_e1 #Htypeof_e2
1035       >Htypeof_e1 >Htypeof_e2
1036       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1037       #Hclassify
1038       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1039       normalize nodelta
1040       whd in match (typ_of_type (Tint ??));
1041       #lhs #rhs #Htyp_should_eq
1042       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1043       -Htyp_should_eq
1044       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1045       <Heq_e' -Heq_e'
1046       #Hexec
1047       #Hexpr_vars_rhs #Hexpr_vars_lhs
1048       #Htranslate_rhs #Htranslate_lhs
1049       * #Hyp_present_lhs #Hyp_present_rhs
1050       #Hind_rhs #Hind_lhs
1051       cases (bind_inversion ????? Hexec) -Hexec
1052       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1053       cases (bind_inversion ????? Hexec) -Hexec
1054       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1055       cases (bind_inversion ????? Hexec) -Hexec
1056       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1057       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1058       whd in match (typeof ?); whd in match (typeof ?);
1059       #Hsem_binary
1060       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1061       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1062       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1063       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1064       whd in match (eval_expr ???????);
1065       whd in match (proj1 ???);
1066       >Heval_lhs normalize nodelta
1067       >Heval_rhs normalize nodelta
1068       whd in match (m_bind ?????);
1069       whd in match (eval_binop ???????);
1070       whd in Hsem_binary:(??%?);
1071       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1072       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1073       cases (sem_mul_inversion … Hsem_binary)
1074       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1075       #Hcm_lhs #Hcm_rhs #Hcm_val
1076       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1077       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1078       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1079       >intsize_eq_elim_true normalize nodelta
1080       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1081       @conj try @refl
1082       whd in Hsem_binary:(??%?);     
1083       whd in match (classify_aop ??) in Hsem_binary:(??%?);
1084       >type_eq_dec_true in Hsem_binary; normalize nodelta
1085       >intsize_eq_elim_true #Heq destruct (Heq)
1086       %2
1087     | 4,5: (* div *)
1088       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1089       [ 2,4: #Hclassify >Hclassify normalize nodelta
1090            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1091       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1092       whd in match (typeof ?); #e'
1093       * #sz * * * *
1094       whd in match (typeof ?) in ⊢ (% → % → ?);
1095       #Htypeof_e1 #Htypeof_e2
1096       >Htypeof_e1 >Htypeof_e2
1097       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1098       #Hclassify
1099       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1100       normalize nodelta
1101       whd in match (typ_of_type (Tint ??));
1102       #lhs #rhs #Htyp_should_eq
1103       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1104       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1105       -Htyp_should_eq
1106       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1107       <Heq_e' -Heq_e'
1108       #Hexec
1109       #Hexpr_vars_rhs #Hexpr_vars_lhs
1110       #Htranslate_rhs #Htranslate_lhs
1111       * #Hyp_present_lhs #Hyp_present_rhs
1112       #Hind_rhs #Hind_lhs
1113       cases (bind_inversion ????? Hexec) -Hexec
1114       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1115       cases (bind_inversion ????? Hexec) -Hexec
1116       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1117       cases (bind_inversion ????? Hexec) -Hexec
1118       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1119       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1120       whd in match (typeof ?); whd in match (typeof ?);
1121       #Hsem_binary
1122       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1123       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1124       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1125       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1126       whd in match (eval_expr ???????);
1127       whd in match (proj1 ???);
1128       >Heval_lhs normalize nodelta
1129       >Heval_rhs normalize nodelta
1130       whd in match (m_bind ?????);
1131       whd in match (eval_binop ???????);
1132       whd in Hsem_binary:(??%?);
1133       [ 1,3: (* div*)
1134          lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1135          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1136          [ cases (sem_div_inversion_s … Hsem_binary)
1137          | cases (sem_div_inversion_u … Hsem_binary) ]
1138       | 2,4: (* mod *)
1139          lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1140          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1141          [ cases (sem_mod_inversion_s … Hsem_binary)
1142          | cases (sem_mod_inversion_u … Hsem_binary) ]
1143       ]
1144       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1145       #Hcm_lhs #Hcm_rhs #Hcm_val
1146       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1147       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1148       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1149       >intsize_eq_elim_true normalize nodelta
1150       [ cases (division_s ???) in Hcm_val;
1151       | cases (division_u ???) in Hcm_val;
1152       | cases (modulus_s ???) in Hcm_val;
1153       | cases (modulus_u ???) in Hcm_val; ]
1154       normalize nodelta
1155       [ 1,3,5,7: @False_ind ]
1156       #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
1157     | 6,7,8: (* and,or,xor *)
1158       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1159       [ 2,4,6: #Hclassify >Hclassify normalize nodelta
1160            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1161       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1162       whd in match (typeof ?); #e'
1163       * #sz * #sg * *
1164       whd in match (typeof ?) in ⊢ (% → % → ?);
1165       #Htypeof_e1 #Htypeof_e2
1166       >Htypeof_e1 >Htypeof_e2
1167       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1168       #Hclassify
1169       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1170       normalize nodelta
1171       whd in match (typ_of_type (Tint ??));
1172       #lhs #rhs #Htyp_should_eq
1173       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1174       -Htyp_should_eq
1175       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1176       <Heq_e' -Heq_e'
1177       #Hexec
1178       #Hexpr_vars_rhs #Hexpr_vars_lhs
1179       #Htranslate_rhs #Htranslate_lhs
1180       * #Hyp_present_lhs #Hyp_present_rhs
1181       #Hind_rhs #Hind_lhs
1182       cases (bind_inversion ????? Hexec) -Hexec
1183       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1184       cases (bind_inversion ????? Hexec) -Hexec
1185       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1186       cases (bind_inversion ????? Hexec) -Hexec
1187       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1188       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1189       whd in match (typeof ?); whd in match (typeof ?);
1190       #Hsem_binary
1191       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1192       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1193       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1194       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1195       whd in match (eval_expr ???????);
1196       whd in match (proj1 ???);
1197       >Heval_lhs normalize nodelta
1198       >Heval_rhs normalize nodelta
1199       whd in match (m_bind ?????);
1200       whd in match (eval_binop ???????);
1201       whd in Hsem_binary:(??%?);
1202       [ 1: (* and *)
1203          lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1204           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1205          cases (sem_and_inversion … Hsem_binary)
1206       | 2: (* or *)
1207          lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1208           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1209          cases (sem_or_inversion … Hsem_binary)
1210       | 3: (* xor *)
1211          lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1212           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1213          cases (sem_xor_inversion … Hsem_binary)
1214       ]
1215       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1216       #Hcm_lhs #Hcm_rhs #Hcm_val
1217       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1218       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1219       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1220       >intsize_eq_elim_true normalize nodelta
1221       [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
1222       | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1223       | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1224       ]
1225       @conj try @refl >Hcm_val %2
1226     | 9,10: (* shl, shr *)
1227       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1228       [ 2,4: #Hclassify >Hclassify normalize nodelta
1229            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1230       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1231       whd in match (typeof ?); #e'
1232       * #sz * * * *
1233       whd in match (typeof ?) in ⊢ (% → % → ?);
1234       #Htypeof_e1 #Htypeof_e2
1235       >Htypeof_e1 >Htypeof_e2
1236       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1237       #Hclassify
1238       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1239       normalize nodelta
1240       whd in match (typ_of_type (Tint ??));
1241       #lhs #rhs #Htyp_should_eq
1242       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1243       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1244       -Htyp_should_eq
1245       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1246       <Heq_e' -Heq_e'
1247       #Hexec
1248       #Hexpr_vars_rhs #Hexpr_vars_lhs
1249       #Htranslate_rhs #Htranslate_lhs
1250       * #Hyp_present_lhs #Hyp_present_rhs
1251       #Hind_rhs #Hind_lhs
1252       cases (bind_inversion ????? Hexec) -Hexec
1253       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1254       cases (bind_inversion ????? Hexec) -Hexec
1255       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1256       cases (bind_inversion ????? Hexec) -Hexec
1257       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1258       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1259       whd in match (typeof ?); whd in match (typeof ?);
1260       #Hsem_binary
1261       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1262       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1263       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1264       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1265       whd in match (eval_expr ???????);
1266       whd in match (proj1 ???);
1267       >Heval_lhs normalize nodelta
1268       >Heval_rhs normalize nodelta
1269       whd in match (m_bind ?????);
1270       whd in match (eval_binop ???????);
1271       whd in Hsem_binary:(??%?);
1272       [ 1,3: (* shl *)
1273          lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1274          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1275          cases (sem_shl_inversion … Hsem_binary)
1276          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1277          #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
1278          destruct (Hcl_lhs Hcl_rhs)
1279          >(value_eq_int_inversion … Hvalue_eq_lhs)
1280          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1281          >Hshift_ok normalize nodelta
1282          %{(Vint sz1
1283               (shift_left bool (bitsize_of_intsize sz1)
1284               (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
1285          @conj try @refl >Hcl_val %2
1286       | *: (* shr, translated to mod /!\ *)     
1287          lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1288          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1289          cases (sem_shr_inversion … Hsem_binary) normalize nodelta
1290          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1291          #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
1292          destruct (Hcl_lhs Hcl_rhs)
1293          >(value_eq_int_inversion … Hvalue_eq_lhs)
1294          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1295          >Hshift_ok normalize nodelta >Hcl_val
1296          /3 by ex_intro, conj, vint_eq/ ]
1297     | *: (* comparison operators *)
1298       lapply e' -e'
1299       cases e1 #ed1 #ety1
1300       cases e2 #ed2 #ety2
1301       whd in match (typeof ?) in ⊢ (% → % → % → %);
1302       #cm_expr whd in match (typeof ?);
1303       inversion (classify_cmp ety1 ety2)
1304       [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
1305            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1306            lapply (jmeq_to_eq ??? Hety1) #Hety2'
1307            destruct #Hclassify >Hclassify normalize nodelta
1308            #cmexpr1 #cmexpr2
1309            whd in ⊢ ((???%) → ?);
1310            #Heq destruct (Heq)
1311       | 1,4,7,10,13,16:
1312            #sz #sg #Hety1 #Hety2 #Hclassify
1313            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1314            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1315            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1316            whd in match (typeof ?) in ⊢ (% → % → % → %);
1317            whd in match (typ_of_type ?) in ⊢ (% → % → ?);
1318            cases sg #cmexpr1 #cmexpr2 normalize nodelta
1319            #Hcast_to_bool #Hexec_expr
1320            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1321            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1322            destruct (Htyis_int)
1323            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1324            destruct (Hcm_expr)
1325            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1326            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1327            cases (bind_inversion ????? Hexec) -Hexec
1328            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1329            cases (bind_inversion ????? Hexec) -Hexec
1330            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1331            lapply (opt_to_res_inversion ???? Hsem) -Hsem           
1332            whd in match (typeof ?); whd in match (sem_binary_operation ???????);
1333            normalize nodelta
1334            #Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp
1335            #cl_val' * #Hsem_cmp #Hcl_val_cast
1336            destruct (Hcl_val_cast)
1337            lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
1338            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
1339            destruct (Hcl_lhs) destruct (Hcl_rhs)
1340            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
1341            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1342            * #Hyp_present_lhs #Hyp_present_rhs
1343            #Hind_rhs #Hind_lhs
1344            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1345            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1346            lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1347            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1348            whd in match (eval_expr ???????);
1349            whd in match (eval_expr ???????);
1350            >Heval_lhs normalize nodelta
1351            >Heval_rhs normalize nodelta
1352            whd in match (m_bind ?????);
1353            whd in match (eval_binop ???????);
1354            >(value_eq_int_inversion … Hvalue_eq_lhs)
1355            >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1356            >intsize_eq_elim_true normalize nodelta
1357            destruct (Heq_bool)
1358            whd in match (eval_unop ????);
1359            whd in match (opt_to_res ???);
1360            whd in match (m_bind ?????);
1361            whd in match (of_bool ?);
1362            [ %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
1363            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
1364            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
1365            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
1366            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
1367            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
1368            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
1369            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
1370            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
1371            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
1372            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))}
1373            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} ]
1374            @conj try @refl
1375            whd in match (FE_of_bool ?); whd in match FEtrue; whd in match FEfalse;
1376            [ 1,3,5,7,9,11:
1377              cases (cmp_int ????) normalize nodelta
1378            | *:
1379              cases (cmpu_int ????) normalize nodelta ]           
1380            try @value_eq_cl_cm_true
1381            try @value_eq_cl_cm_false
1382       | *: (* ptr comparison *)
1383            #n #ty' #Hety1 #Hety2 #Hclassify
1384            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1385            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1386            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1387            whd in match (typeof ?) in ⊢ (% → % → % → %);
1388            #cmexpr1 #cmexpr2
1389            #Hcast_to_bool #Hexec_expr
1390            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1391            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1392            destruct (Htyis_int)
1393            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1394            destruct (Hcm_expr)
1395            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1396            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1397            cases (bind_inversion ????? Hexec) -Hexec
1398            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1399            cases (bind_inversion ????? Hexec) -Hexec
1400            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1401            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1402            whd in match (typeof ?); whd in match (sem_binary_operation ???????);
1403            #Hsem_cmp
1404            cases (some_inversion ????? Hsem_cmp) -Hsem_cmp normalize nodelta
1405            #cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast);
1406            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1407            * #Hyp_present_lhs #Hyp_present_rhs
1408            #Hind_rhs #Hind_lhs
1409            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
1410            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs
1411            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
1412            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs -Hexec_lhs
1413            lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) -Hsem_cmp
1414            -Hvalue_eq_lhs -Hvalue_eq_rhs
1415            * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res
1416            whd in match (eval_expr ???????);
1417            whd in match (eval_expr ???????);
1418            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1419            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1420            whd in match (m_bind ?????);           
1421            lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm
1422            *
1423            [ 2,4,6,8,10,12:
1424              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1425              whd in Hsem_cmp:(??%?); destruct
1426            | *: *
1427              [ 2,4,6,8,10,12:
1428                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1429                whd in Hsem_cmp:(??%?); destruct
1430              | *: *
1431                [ 2,4,6,8,10,12:
1432                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1433                  whd in Hsem_cmp:(??%?); destruct
1434                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome
1435                     whd in Hsem_cmp:(??%?); destruct
1436                ]
1437              ]
1438            ]
1439            whd in match (eval_binop ???????);
1440            normalize nodelta
1441            whd in match (eval_unop ????);
1442            whd in match (opt_to_res ???);
1443            whd in match (m_bind ?????);
1444            [ 1,2,3,4,5,6:
1445              [ 1,4,6:
1446                %{(zero_ext tysz FEtrue)} @conj try @refl
1447                >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1448                @value_eq_cl_cm_true
1449              | 2,3,5:
1450                %{(zero_ext tysz FEfalse)} @conj try @refl
1451                >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1452                @value_eq_cl_cm_false
1453              ]
1454            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
1455                 lapply Heq_block_outcome -Heq_block_outcome
1456                 @(eq_block_elim … (pblock p1) (pblock p2))
1457                 normalize nodelta
1458                 whd in match (eval_unop ????);
1459                 whd in match (opt_to_res ???);
1460                 whd in match (m_bind ?????);
1461                 [ 1,3,5,7,9,11:
1462                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
1463                   whd in match (eval_unop ????);
1464                   whd in match (m_bind ?????);
1465                   cases (cmp_offset ???) in Hvalue_eq_res; normalize nodelta
1466                   #Hvalue_eq_res >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1467                   [ 1,3,5,7,9,11: %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
1468                                   @value_eq_cl_cm_true
1469                   | 2,4,6,8,10,12: %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
1470                                    @value_eq_cl_cm_false
1471                   ]
1472                 | *:
1473                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1474                   >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1475                   [ %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
1476                     @value_eq_cl_cm_false
1477                   | %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
1478                     @value_eq_cl_cm_true
1479                   ]
1480                ]
1481           ]
1482       ]
1483    ]
1484
1485| 1: (* Integer constant *)
1486  #csz #ty cases ty
1487  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1488  | #structname #fieldspec | #unionname #fieldspec | #id ]
1489  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
1490  #val #trace #Hpresent #Hexec_cl
1491  whd in Htranslate:(??%?);
1492  [ 1,3,4,5,6,7,8: destruct ]
1493  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))))
1494  [ 2: * #H_err #H_neq_sz
1495       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1496       >Htranslate #Habsurd destruct (Habsurd) ]
1497  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1498  destruct (Heq_sz)
1499  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
1500  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
1501  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
1502| 2: *
1503  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
1504  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1505  try /2 by I/
1506  #ty whd in ⊢ (% → ?); #Hind
1507  whd in match (Plvalue ???);
1508  whd in match (typeof ?);
1509  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
1510  whd in Hexec:(??%?);
1511  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
1512  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
1513  whd in Hcl_success:(???%);
1514  [ 1: (* var case *)
1515       lapply Hcl_success -Hcl_success -Hind
1516       (* Peform case analysis on presence of variable in local Clight env.
1517        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
1518       @(match lookup SymbolTag block cl_env var_id
1519         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
1520         with
1521         [ None ⇒ λHcl_lookup. ?
1522         | Some loc ⇒ λHcl_lookup. ?
1523         ] (refl ? (lookup SymbolTag block cl_env var_id)))
1524       normalize nodelta
1525       [ 1: (* global case *)
1526            #Hlookup_global
1527            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
1528            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
1529            #Heq whd in Heq:(???%); destruct (Heq)
1530            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1531            * #var_id_alloctype * #var_id_type * #Heq
1532            cases (variable_not_in_env_but_in_vartypes_is_global …
1533                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
1534            #r #Heq' destruct (Heq') normalize nodelta
1535            lapply Hcl_load_success -Hcl_load_success
1536            lapply Hyp_present -Hyp_present
1537            lapply Hexpr_vars -Hexpr_vars
1538            lapply cm_expr -cm_expr inversion (access_mode ty)
1539            [ #typ_of_ty | | #typ_of_ty ]
1540            #Heq_typ_of_type #Heq_access_mode
1541            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1542            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1543            whd in match (eval_expr ???????);
1544            whd in match (eval_expr ???????);
1545            whd in match (eval_constant ????);
1546            <(eq_sym … inv) >Hfind_symbol normalize nodelta
1547            cases (bind_inversion ????? Hcl_load_success) #x *
1548            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
1549            lapply (opt_to_res_inversion ???? Hopt_to_res)
1550            #Hcl_load_success
1551            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1552                 @conj try @refl
1553                 whd in Hcm_load_success:(??%?);
1554                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
1555                 >(load_value_of_type_by_ref … Hcl_load_success)
1556                 try assumption %4
1557                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1558                 >Hfind_symbol normalize nodelta #Heq_embedding
1559                 whd in match (shift_offset ???);
1560                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
1561                 normalize nodelta @refl
1562            | 1: cut (access_mode ty=By_value (typ_of_type ty))
1563                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
1564                   lapply Heq_access_mode <Heqt // ] #Haccess
1565                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
1566                 #Hvalid_ptr
1567                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
1568                 [ whd in ⊢ (??%?);
1569                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1570                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
1571                 * #val' * #Hcm_load_success #Hvalue_eq
1572                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
1573                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
1574                 normalize %{val'} @conj try @refl assumption ]
1575       | 2: (* local case *)
1576            #Heq destruct (Heq)
1577            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1578            * #var_id_alloc_type * #var_id_type *
1579            generalize in match var_id_alloc_type; * normalize nodelta
1580            [ 1: #r #Hlookup_vartype
1581                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
1582                 * #typ whd in match (local_id ???);
1583                 >Hlookup_vartype normalize nodelta @False_ind
1584            | 2: (* Stack local *)
1585                 lapply Hcl_load_success -Hcl_load_success
1586                 lapply Hyp_present -Hyp_present
1587                 lapply Hexpr_vars -Hexpr_vars
1588                 lapply cm_expr -cm_expr inversion (access_mode ty)
1589                 [ #typ_of_ty | | #typ_of_ty ]
1590                 #Heq_typ_of_type #Heq_access_mode
1591                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
1592                 #stack_depth #Hlookup_vartype_success normalize nodelta
1593                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1594                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1595                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
1596                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1597                 >Hlookup' normalize nodelta #Hembedding_eq
1598                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1599                 #loaded_val * #Hload_val
1600                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1601                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1602                 #Hload_success whd in match (eval_expr ???????);
1603                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
1604                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
1605                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
1606                        >offset_plus_0 @refl ]
1607                 #Hpointer_translation
1608                 [ 2: (* By-ref *)
1609                      whd in Hload_success:(??%?);
1610                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
1611                      #Heq_val
1612                      >Heq_val
1613                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
1614                      @conj try @refl
1615                      %4 whd in match (shift_offset ???);
1616                      whd in match zero_offset;
1617                      >commutative_addition_n >addition_n_0 @Hpointer_translation
1618                 | 1: (* By value *)
1619                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
1620                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
1621                      [ @(load_by_value_success_valid_pointer … Hload_success)
1622                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
1623                      * #cm_val * #Hload_in_cm #Hvalue_eq
1624                      %{cm_val} @conj try assumption
1625                      lapply (load_value_of_type_by_value … Hload_in_cm)
1626                      [ lapply Heq_access_mode <Heq0 #Heq1
1627                        @(jmeq_to_eq ??? Heq1) ]
1628                      #Hloadv <Heq0
1629                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
1630                      >Hloadv @refl ]
1631            | 3: (* Register local variable *)
1632                 #Hlookup_eq
1633                 lapply (res_inversion ?????? Hlookup_eq)
1634                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1635                 #Htype_eq
1636                 cases (type_should_eq_inversion
1637                            var_id_type
1638                            ty
1639                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
1640                            … Htype_eq) -Htype_eq
1641                 (* Reverting all premises in order to perform type rewrite *)
1642                 #Htype_eq
1643                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
1644                 lapply Hcl_load_success -Hcl_load_success
1645                 lapply Hcl_lookup -Hcl_lookup
1646                 lapply Hyp_present -Hyp_present
1647                 lapply Hexpr_vars -Hexpr_vars
1648                 lapply cm_expr
1649                 destruct (Htype_eq)
1650                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
1651                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
1652                 destruct (Hexpr_eq)
1653                 whd in match (eval_expr ???????);
1654                 whd in match (lookup_present ?????);
1655                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1656                 >Hlookup' normalize nodelta #Hmatching
1657                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1658                 #loaded_val * #Hload_val
1659                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1660                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1661                 #Hload_success
1662                 cases (Hmatching … Hload_success) #val'
1663                 * #Hlookup_in_cm #Hvalue_eq %{val'}
1664                 cases Hyp_present
1665                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
1666                 (* seems ok *)
1667            ]
1668       ]
1669  | 2: lapply Hcl_success -Hcl_success
1670       lapply Htranslate_expr -Htranslate_expr
1671       lapply Hind -Hind cases ty1
1672       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1673       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1674       #Hind #Htranslate_expr #Hexec_cl
1675       cases (bind_inversion ????? Htranslate_expr) (* -Htranslate_expr *)
1676       * whd in match (typ_of_type ?); normalize nodelta
1677       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
1678       whd in ⊢ ((???%) → ?);
1679       [ 1,2,6,7: #Heq destruct (Heq) ]
1680       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
1681       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
1682       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
1683       [ 1,3,5,7: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ]
1684       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
1685       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
1686       #Hexec_cl_ind #Hcl_ptr
1687       cut (∃ptr. cl_ptr = Vptr ptr)
1688       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
1689                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
1690       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
1691       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
1692       #Hind lapply (Hind (refl ??)) -Hind
1693       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
1694       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
1695       destruct (Hcm_ptr) #Hpointer_translation
1696       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
1697       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
1698       -Hopt_to_res
1699       lapply Hexec_cm_ind -Hexec_cm_ind
1700       lapply Hyp_present -Hyp_present
1701       lapply Htranslate_expr -Htranslate_expr
1702       lapply Hexpr_vars -Hexpr_vars
1703       lapply cm_expr -cm_expr
1704       cases ty (* Inversion (access_mode ty) fails for whatever reason. *)
1705       [ | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
1706       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
1707       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
1708       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 ]
1709       whd in match (typ_of_type ?); whd in match (access_mode ?); normalize nodelta
1710       #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_cm_ind #Hcl_load_success
1711       #Heq destruct (Heq)
1712       [ 3,4,8,9,13,14,18,19: (*  By reference *)
1713           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1714           lapply (load_value_of_type_by_ref … Hcl_load_success ??)
1715           try @refl_jmeq
1716           #Hval >Hval %4 assumption
1717       | *: (* By_value *)
1718           (* project Hcl_load_success in Cminor through memory_inj *)
1719           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
1720           try @(load_by_value_success_valid_pointer … Hcl_load_success)
1721           try @jmeq_to_eq
1722           try assumption try @refl_jmeq
1723           * #cm_val * #Hcm_load_success #Hvalue_eq
1724           lapply (load_value_of_type_by_value … Hcm_load_success)
1725           try @refl
1726           #Hloadv_cm
1727           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
1728           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption ]
1729  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
1730       lapply (refl ? (typeof e1))
1731       cases (typeof e1) in ⊢ ((???%) → %);
1732       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1733       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
1734       #Heq_typeof normalize nodelta
1735       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
1736       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
1737       normalize nodelta #Htranslate_expr
1738       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1739       * whd in match (typ_of_type ?); normalize nodelta
1740       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
1741       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
1742         #cm_field_off * #Hcm_field_off
1743       | lapply Htranslate_expr2 -Htranslate_expr2 ]
1744       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1745       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
1746       whd in Hexec_lvalue:(???%);
1747       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1748         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
1749       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1750       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1751       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
1752       [  (* Struct case *)
1753         lapply Hcl_load_value -Hcl_load_value
1754         lapply Hyp_present -Hyp_present
1755         lapply Hexpr_vars -Hexpr_vars
1756         lapply cm_expr -cm_expr
1757         lapply Hind -Hind
1758         cases ty
1759         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1760         | #structname #fieldspec | #unionname #fieldspec | #id ]
1761         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1762         normalize nodelta
1763         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1764         whd in match (eval_expr ???????);
1765         (* applying the arguments of the induction hypothesis progressively *)
1766         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind
1767                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
1768         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
1769         lapply (Hind ?)
1770         [ 1,3,5,7,9:
1771            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1772            >Htranslate_expr_ind whd in match (m_bind ?????);
1773            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
1774         whd in Hoffset_eq:(???%); destruct (offset_eq)
1775         cut (cl_field_off = cm_field_off)
1776         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
1777           normalize #Heq destruct (Heq) @refl ]
1778         #Heq destruct (Heq)
1779         lapply (Hind cl_b cl_o trace ?)
1780         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
1781         lapply (Hind ?) -Hind
1782         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1783           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
1784           @Hoffset_eq ]
1785         * #cm_val' * #Heval_expr #Hvalue_eq
1786         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
1787         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
1788         [ 1,2,5: (* by-value *)
1789            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
1790            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1791            * #cm_val * #Hcm_load_value #Hvalue_eq
1792            lapply (load_value_of_type_by_value … Hcm_load_value)
1793            [ 1,3,5: @refl ]
1794            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
1795            try @refl try assumption
1796         | 3,4: (* by-ref *)
1797            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
1798            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1799            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
1800         ]
1801      | (* union case *)
1802         lapply Hcl_load_value -Hcl_load_value
1803         lapply Hyp_present -Hyp_present
1804         lapply Hexpr_vars -Hexpr_vars
1805         lapply cm_expr -cm_expr
1806         lapply Hind -Hind
1807         cases ty
1808         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1809         | #structname #fieldspec | #unionname #fieldspec | #id ]
1810         whd in match (typ_of_type ?); normalize nodelta
1811         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1812         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1813         [ 1,2,5: (* by-value *)
1814            whd in match (eval_expr ???????);
1815            lapply (Hind cm_expr_ind Hexpr_vars ?)
1816            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
1817            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1818            -Hind #Hind
1819            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
1820            whd in match (m_bind ?????); #Hind
1821            cases (Hind (refl ??)) -Hind
1822            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
1823            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
1824            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
1825            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
1826            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1827            * #cm_val * #Hcm_load_value #Hvalue_eq           
1828            lapply (load_value_of_type_by_value … Hcm_load_value)
1829            [ 1,3,5: @refl ]
1830            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
1831            try @refl assumption
1832         | 3,4:
1833            whd in Hexec_cl:(???%); destruct (Hexec_cl)
1834            lapply (Hind cm_expr Hexpr_vars)
1835            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
1836            lapply (Hind Htranslate_expr_ind) -Hind
1837            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1838            >Hexec_lvalue whd in match (m_bind ?????);
1839            #Hind cases (Hind … Hyp_present (refl ??))
1840            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
1841            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
1842            assumption ]
1843    ]
1844  ]
1845| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
1846     whd in Hexec_lvalue_var:(??%?);
1847     (* check whether var is local or global *)
1848     lapply (Hlocal_matching var)
1849     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
1850     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
1851     normalize nodelta
1852     [ 1: (* global *)
1853          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
1854          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
1855          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
1856          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
1857          #Hembed
1858          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1859          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
1860          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
1861          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1862          whd in match (eval_expr ???????);
1863          whd in match (eval_constant ????);
1864          <(eq_sym inv var) >Hfind_symbol normalize nodelta
1865          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1866          @conj try @refl %4 whd in match (pointer_translation ??);
1867          >Hembed normalize nodelta whd in match (shift_offset ???);
1868          >addition_n_0 @refl
1869     | 2: (* local *)
1870          #BL #Heq destruct (Heq) #_
1871          @(match (lookup ?? vars var)
1872            return λx. (lookup ?? vars var = x) → ?
1873            with
1874            [ None ⇒ ?
1875            | Some kind ⇒ ?
1876            ] (refl ??))
1877          normalize nodelta
1878          #Hlookup [ @False_ind ]
1879          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
1880          #Hlookup
1881          lapply (refl ? var_alloctype)
1882          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
1883          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
1884          [ (* stack alloc*)
1885            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1886            * #var_alloctype' #var_type' * #Hlookup_vartype'           
1887            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1888            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1889            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
1890            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
1891            @conj try @refl %4 whd in match (pointer_translation ??);
1892            >Hembed @refl
1893          | (* local alloc *)
1894            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1895            * #var_alloctype' #var_type' * #Hlookup_vartype'
1896            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1897            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1898            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
1899(*| 4: #e #ty*)
1900| 4:
1901  * #ed #ety cases ety
1902  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1903  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
1904  whd in match (typeof ?);
1905  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
1906  cases (bind_inversion ????? Htranslate) -Htranslate   
1907  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1908  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1909  * #cl_val #trace0 * #Hexec_expr #Hcl_val
1910  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
1911  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1912  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
1913  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
1914    [ 1,5,9,13: #Heq destruct (Heq)
1915    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
1916    | 3,7,11,15: #Heq destruct (Heq)
1917    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
1918  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
1919  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
1920  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
1921  %{cm_val} @conj try @refl try assumption
1922| 5:
1923  #ty cases ty
1924  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1925  | #structname #fieldspec | #unionname #fieldspec | #id ]
1926  #ed #ty' #Hind
1927  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
1928  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1929  cases (bind_inversion ????? Htranslate) -Htranslate
1930  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1931  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1932  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
1933  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1934  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1935  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
1936  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
1937  %{cm_val} @conj try @refl assumption
1938| 6:
1939  #ty *
1940  [ cases ty
1941    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1942    | #structname #fieldspec | #unionname #fieldspec | #id ]
1943    #e #Hind
1944    whd in match (typeof ?);
1945    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
1946    #Htranslate
1947    [ 3,4,5,8: destruct (Htranslate)
1948    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1949         cases sz normalize nodelta
1950         #e' #Hexpr_vars #Htranslate
1951         [ 1, 2: destruct (Htranslate) ] ]
1952    #cl_val #trace #Hyp_present #Hexec_expr
1953    cases (bind_inversion ????? Htranslate) -Htranslate
1954    #cmop * #Htranslate_unop #Hexec_arg
1955    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1956    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1957    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1958    * #cl_arg #cl_trace * #Hexec_cl
1959    whd in ⊢ ((???%) → ?); #Hexec_unop
1960    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1961    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1962    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1963    #Hsem_cl whd in match (eval_expr ???????);
1964    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1965    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1966    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
1967    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
1968    whd in match (typ_of_type Tvoid);
1969    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
1970    #H >H @refl
1971  | *:
1972    cases ty
1973    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
1974    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
1975    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
1976    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
1977    whd in Htranslate:(??%?);
1978    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
1979    cases (bind_inversion ????? Htranslate) -Htranslate
1980    #cmop * #Htranslate_unop #Hexec_arg
1981    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1982    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1983    cases (bind_inversion ????? Hexec) -Hexec
1984    * #cl_arg #cl_trace * #Hexec_cl
1985    whd in ⊢ ((???%) → ?); #Hexec_unop
1986    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1987    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1988    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1989    #Hcl_unop whd in match (eval_expr ???????);
1990    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1991    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1992    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
1993    * #op_res * #Hcl_sem #Hvalue_eq
1994    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
1995       %{op_res} @conj try @refl assumption
1996    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
1997       %{op_res} @conj try @refl assumption
1998    ]
1999  ]
2000| 8: #ty #ty' * #ed #ety
2001  cases ety
2002  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2003  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2004  whd in match (typeof ?); whd in match (typ_of_type ?);
2005  #Hind whd in match (typeof ?);
2006  #cm_expr #Hexpr_vars #Htranslate
2007  cases (bind_inversion ????? Htranslate) -Htranslate
2008  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
2009  cases (bind_inversion ????? Htranslate) -Htranslate
2010  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
2011  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
2012  cases (bind_inversion ????? Htranslate) -Htranslate
2013  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
2014  #Heq destruct (Heq)
2015  #cl_val #trace #Hyp_present #Hexec_cm
2016  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2017  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
2018  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
2019  #cast_val * #Hexec_cast
2020  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2021  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
2022  #Htype_eq
2023  lapply Hexec_cast -Hexec_cast
2024(*  lapply Htyp_should_eq -Htyp_should_eq *)
2025  lapply Htranslate_cast -Htranslate_cast
2026  lapply Hexpr_vars_cast -Hexpr_vars_cast
2027  lapply cm_cast -cm_cast
2028  lapply Hyp_present -Hyp_present
2029  lapply Hexpr_vars -Hexpr_vars
2030  lapply cm_expr -cm_expr
2031  <Htype_eq -Htype_eq
2032  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
2033  whd in match (typeof ?); normalize nodelta
2034  cases ty'
2035  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2036  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2037  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2038  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
2039  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2040  whd in Htranslate_cast:(??%%);
2041  whd in Hexpr_vars;
2042  destruct (Htranslate_cast)
2043  [ 1,2,3,4,7:
2044    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2045    * #cm_val' * #Heval_castee
2046    lapply Hexec_cm -Hexec_cm
2047    whd in Hexec_cast:(??%%);
2048    cases cm_val in Hexec_cast; normalize nodelta
2049    [ | #vsz #vi | | #vp
2050    | | #vsz #vi | | #vp
2051    | | #vsz #vi | | #vp
2052    | | #vsz #vi | | #vp
2053    | | #vsz #vi | | #vp ]
2054    [ 2,6,10,14,18:
2055    | *: #Habsurd destruct (Habsurd) ]
2056    #Hexec_cast #Hexec_cm #Hvalue_eq
2057    [ 1,2,3:
2058      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
2059      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
2060    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
2061    [ 1,2,4,5:
2062      cases (bind_inversion ????? Hexec_cast)
2063      whd in match (typeof ?);
2064      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
2065      whd in match (eq_rect_r ??????);
2066      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
2067      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
2068      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
2069      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
2070      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2071      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
2072      >Heval_castee normalize nodelta whd in match (eval_unop ????);
2073      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
2074      >Heq_vi >eq_bv_true normalize
2075      %{Vnull} @conj try @refl %3
2076    | 3: destruct (Hcl_val_eq)
2077          whd in match (eval_expr ???????);
2078          >Heval_castee normalize nodelta
2079          whd in match (eval_unop ????);
2080          cases esg normalize nodelta
2081          whd in match (opt_to_res ???); whd in match (m_bind ?????);
2082          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
2083          whd in match (eq_rect_r ??????);
2084          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
2085          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
2086             this reason. *)
2087          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
2088          cases esz normalize nodelta
2089          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
2090          whd in match (sign_ext ??); whd in match (zero_ext ??);
2091          %2
2092    ]
2093 | *:
2094    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2095    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
2096    %{cm_val'} @conj try @refl
2097    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
2098    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
2099    cases cm_val
2100    [ | #vsz #vi | | #vp
2101    | | #vsz #vi | | #vp
2102    | | #vsz #vi | | #vp
2103    | | #vsz #vi | | #vp ]
2104    #Hexec_cm #Hvalue_eq #Hexec_cast
2105    whd in Hexec_cast:(??%%);
2106    [ 1,5,9,13: destruct (Hexec_cast) ]
2107    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
2108    lapply Hexec_cast -Hexec_cast
2109    normalize cases (eq_v ?????) normalize
2110    #Habsurd destruct (Habsurd)
2111 ]
2112| 9: (* Econdition *) 
2113  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
2114  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
2115  #Hexec_cm
2116  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2117  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
2118  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2119  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
2120  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2121  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
2122  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2123  cases (bind_inversion ????? Htranslate) -Htranslate
2124  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2125  cases (bind_inversion ????? Htranslate) -Htranslate
2126  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2127  cases (bind_inversion ????? Htranslate) -Htranslate
2128  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
2129  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
2130  *  #Htypeof_e2_eq_ty
2131  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2132  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
2133  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
2134  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2135  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
2136  cases (bind_inversion ????? Htranslate) -Htranslate
2137  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
2138  cases (bind_inversion ????? Htranslate) -Htranslate 
2139  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
2140  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
2141  * #Htypeof_e3_eq_ty
2142  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
2143  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
2144  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
2145  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2146  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
2147  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
2148  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
2149  lapply Hexec_bool_of_val -Hexec_bool_of_val
2150  cases (typeof e1) normalize nodelta
2151  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2152  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2153  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
2154  whd in Heq:(???%); destruct (Heq)
2155  whd in match (eval_expr ???????);
2156  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
2157  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
2158  >Heval_e1 normalize nodelta
2159  lapply Hcm_ifthenelse -Hcm_ifthenelse
2160  lapply Hexec_cond -Hexec_cond 
2161  lapply Hexec_bool_of_val -Hexec_bool_of_val
2162  lapply Hvalue_eq1 -Hvalue_eq1
2163  cases cm_cond_val
2164  [ | #vsz #vi | | #vp
2165  | | #vsz #vi | | #vp
2166  | | #vsz #vi | | #vp
2167  | | #vsz #vi | | #vp ]
2168  whd in ⊢ (? → (??%%) → ?);
2169  [ 6:
2170  | *: #_ #Habsurd destruct (Habsurd) ]
2171  #Hvalue_eq1 #Hsz_check
2172  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2173  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2174  #Heq destruct (Heq)
2175  #Hexec_expr_e1
2176  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
2177    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
2178    with
2179    [ true ⇒ λHeq. ?
2180    | false ⇒ λHeq. ?
2181    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
2182  normalize nodelta
2183  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
2184  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
2185  >Heq normalize nodelta
2186  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
2187    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
2188    normalize %{cm_val3} @conj try @refl assumption
2189  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
2190    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
2191    normalize %{cm_val2} @conj try @refl assumption ]
2192| 10: (* andbool *)
2193  #ty
2194  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2195  cases ty
2196  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2197  | #structname #fieldspec | #unionname #fieldspec | #id ]
2198  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2199  (* decompose first slice of clight execution *)
2200  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2201  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2202  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2203(* cut *) 
2204  * * normalize nodelta #Hexec_bool_of_val
2205  [ 2,4,6,8,10,12,14:
2206    whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2207  | 16: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
2208  | *:
2209    #Hexec_expr   
2210    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2211    * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
2212    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2213    #b2 * #Hexec_bool_of_val_e2
2214    whd in ⊢ ((???%) → ?); #Heq
2215    destruct (Heq) ]
2216  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2217  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2218  cases (bind_inversion ????? Htranslate) -Htranslate
2219  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2220  cases (bind_inversion ????? Htranslate) -Htranslate
2221  * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
2222  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
2223  * #Htypeof_e2_eq_ty
2224  (* cleanup the type coercion *)
2225  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2226  lapply Hexpr_vars_wt -Hexpr_vars_wt
2227  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2228  lapply Hexpr_vars_e2 -Hexpr_vars_e2
2229  lapply cm_expr_e2 -cm_expr_e2
2230  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
2231  #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2232
2233  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2234  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2235  lapply Hexpr_vars_e1 -Hexpr_vars_e1
2236  lapply cm_expr_e1 -cm_expr_e1
2237  cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
2238  [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2239         destruct >(Htypeof_e1) whd in match (typ_of_type ?);
2240         #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2241         whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
2242  *
2243  [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2244         destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
2245         #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
2246         #Habsurd destruct (Habsurd) ]
2247  * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
2248  destruct >Htypeof_e1 #Heq_bv
2249  whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
2250  #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2251  whd in match (typ_of_type ?);
2252  whd in ⊢ ((???%) → ?); #Heq 
2253  destruct (Heq) cases Hyp_present -Hyp_present
2254  * #Hyp_present_e1 * * #Hyp_present_e2 normalize in ⊢ (% → % → % → ?);
2255  * * *
2256  lapply (Hind1 … Hyp_present_e1 Hexec_e1)
2257  * #cm_val_1 * #Heval_expr1 #Hvalue_eq
2258  whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (proj2 ???);
2259  >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
2260  whd in match (eval_bool_of_val ?);
2261  <Heq_bv
2262  whd in match (m_bind ?????);
2263  [ %{(Vint sz (zero (bitsize_of_intsize sz)))}
2264    >zero_ext_zero @conj try %2
2265    whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
2266  normalize nodelta
2267  lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
2268  -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
2269  whd in match (eval_expr ???????); >Heval_expr2
2270  normalize nodelta
2271  cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
2272  [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
2273       destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
2274       #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
2275       whd in match (eval_bool_of_val ?);
2276       whd in match (m_bind ?????); normalize nodelta
2277       >zero_ext_one
2278       %{(Vint sz (repr sz 1))} @conj try %2
2279       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2280  *
2281  [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
2282      >(value_eq_null_inversion … Hvalue_eq2)
2283      whd in match (eval_bool_of_val ?);
2284      whd in match (m_bind ?????);
2285      normalize nodelta
2286      %{(Vint sz (zero (bitsize_of_intsize sz)))}
2287      >zero_ext_zero @conj try %2
2288      whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2289  * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
2290  destruct (Hcl_val_e2)
2291  >(value_eq_int_inversion … Hvalue_eq2)
2292  whd in match (eval_bool_of_val ?); <Heq_bv
2293  cases b2 in Heq_bv; #Heq_bv
2294  whd in match (m_bind ?????); normalize nodelta
2295  [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
2296    >append_nil @conj try @refl >zero_ext_one %2
2297  | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
2298    >append_nil @conj try @refl >zero_ext_zero %2 ]
2299| 11: (* orbool, similar to andbool *)
2300  #ty
2301  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2302  cases ty
2303  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2304  | #structname #fieldspec | #unionname #fieldspec | #id ]
2305  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2306  (* decompose first slice of clight execution *)
2307  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2308  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2309  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2310  * * normalize nodelta #Hexec_bool_of_val
2311  [ 1,3,5,7,9,11,13,15:
2312    whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2313  | *:
2314    #Hexec_expr   
2315    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2316    * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
2317    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2318    #b2 * #Hexec_bool_of_val_e2
2319    whd in ⊢ ((???%) → ?); #Heq
2320    destruct (Heq) ]
2321  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2322  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2323  cases (bind_inversion ????? Htranslate) -Htranslate
2324  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2325  cases (bind_inversion ????? Htranslate) -Htranslate
2326  * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
2327  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
2328  * #Htypeof_e2_eq_ty
2329  (* cleanup the type coercion *)
2330  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2331  lapply Hexpr_vars_wt -Hexpr_vars_wt
2332  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2333  lapply Hexpr_vars_e2 -Hexpr_vars_e2
2334  lapply cm_expr_e2 -cm_expr_e2
2335  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
2336  #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2337  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2338  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2339  lapply Hexpr_vars_e1 -Hexpr_vars_e1
2340  lapply cm_expr_e1 -cm_expr_e1
2341  cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
2342  [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2343         destruct >(Htypeof_e1) whd in match (typ_of_type ?);
2344         #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2345         whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
2346  *
2347  [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2348         destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
2349         #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
2350         #Habsurd destruct (Habsurd) ]
2351  * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
2352  destruct >Htypeof_e1 #Heq_bv
2353  whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
2354  #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2355  whd in ⊢ ((???%) → ?); #Heq
2356  destruct (Heq) cases Hyp_present -Hyp_present
2357  * #Hyp_present_e1 * * * #Hyp_present_e2 * *
2358  lapply (Hind1 … Hyp_present_e1 Hexec_e1)
2359  * #cm_val_1 * #Heval_expr1 #Hvalue_eq
2360  whd in match (eval_expr ???????);
2361  >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
2362  whd in match (eval_bool_of_val ?);
2363  <Heq_bv
2364  whd in match (m_bind ?????);
2365  [ %{(Vint sz (repr sz 1))}
2366    >zero_ext_one @conj try %2
2367    whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
2368  normalize nodelta
2369  lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
2370  -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
2371  whd in match (eval_expr ???????); >Heval_expr2
2372  normalize nodelta
2373  cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
2374  [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
2375       destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
2376       #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
2377       whd in match (eval_bool_of_val ?);
2378       whd in match (m_bind ?????); normalize nodelta
2379       >zero_ext_one
2380       %{(Vint sz (repr sz 1))} @conj try %2
2381       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2382  *
2383  [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
2384      >(value_eq_null_inversion … Hvalue_eq2)
2385      whd in match (eval_bool_of_val ?);
2386      whd in match (m_bind ?????);
2387      normalize nodelta
2388      %{(Vint sz (zero (bitsize_of_intsize sz)))}
2389      >zero_ext_zero @conj try %2
2390      whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2391  * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
2392  destruct (Hcl_val_e2)
2393  >(value_eq_int_inversion … Hvalue_eq2)
2394  whd in match (eval_bool_of_val ?); <Heq_bv
2395  cases b2 in Heq_bv; #Heq_bv
2396  whd in match (m_bind ?????); normalize nodelta
2397  [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
2398    >append_nil @conj try @refl >zero_ext_one %2
2399  | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
2400    >append_nil @conj try @refl >zero_ext_zero %2 ]
2401| 12: (* sizeof *)
2402  #ty cases ty
2403  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2404  | #structname #fieldspec | #unionname #fieldspec | #id ]
2405  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2406  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
2407  normalize in match (typ_of_type ?);
2408  whd in Htranslate:(??%?); destruct (Htranslate)
2409  whd in match (eval_expr ???????);
2410  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
2411| 13:
2412  #ty #ed #ty' cases ty'
2413  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2414  | #structname #fieldspec | #unionname #fieldspec | #id ]
2415  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2416  #Hexec_lvalue
2417  whd in Hexec_lvalue:(??%?); destruct
2418  [ whd in Htranslate_addr:(??%?);
2419    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2420    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
2421    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2422    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
2423    #Heq destruct (Heq)
2424    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
2425  ]
2426  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2427  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
2428  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
2429       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
2430       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
2431       #cm_val_field * #Heval_cm #Hvalue_eq
2432       whd in match (eval_expr ???????);
2433       >Heval_cm normalize nodelta
2434       whd in match (eval_expr ???????); whd in match (m_bind ?????);
2435       whd in match (eval_binop ???????); normalize nodelta
2436       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
2437       normalize nodelta #Hptr_translate
2438       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
2439       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
2440       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
2441       cases (E cl_blo) in Hptr_translate; normalize nodelta
2442       [ #H destruct (H) ]
2443       * #BL #OFF normalize nodelta #Heq destruct (Heq)
2444       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
2445       #H destruct (H)       
2446       whd in match (shift_pointer ???);
2447       whd in match (shift_offset ???) in ⊢ (???%);
2448       >sign_ext_same_size
2449       whd in match (offset_plus ??) in ⊢ (??%%);
2450       <(associative_addition_n ? (offv off))
2451       >(commutative_addition_n … (repr I16 field_off) (offv OFF))
2452       >(associative_addition_n ? (offv off))
2453       @refl       
2454  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
2455       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
2456       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
2457       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
2458       #Hpointer_translation
2459       %{cm_val} @conj try assumption
2460       destruct @refl
2461   ]
2462| 14: (* cost label *)
2463  #ty (* cases ty
2464  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2465  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
2466  #l * #ed #ety
2467  whd in match (typeof ?); whd in match (typeof ?);
2468  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2469  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2470  #Hexpr_vars * #Htranslate_ind #Htranslate
2471  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2472  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2473  whd in match (typeof ?) in Htyp_should_eq:(??%?);
2474  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
2475  #Htyp_eq
2476  lapply Htranslate_ind -Htranslate_ind
2477  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2478  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2479  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2480  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
2481  <Htyp_eq
2482  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
2483  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2484  whd in match (eval_expr ???????);
2485  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2486  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2487  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2488  #cm_val' * #Heval_expr' #Hvalue_eq
2489  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
2490  >cons_to_append >(nil_append … cm_trace) @refl
2491| 15: *
2492  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
2493  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
2494  #ty normalize in ⊢ (% → ?);
2495  [ 2,3,12: @False_ind
2496  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2497           normalize #Habsurd destruct (Habsurd) ]
2498] qed.
2499
2500
2501axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
2502
2503(* Conjectured simulation results
2504
2505   We split these based on the start state:
2506   
2507   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
2508      normal steps in Cminor;
2509   2. call and return steps are simulated by a call/return step plus [m] normal
2510      steps (to copy stack allocated parameters / results); and
2511   3. lone cost label steps are simulates by a lone cost label step
2512   
2513   These should allow us to maintain enough structure to identify the Cminor
2514   subtrace corresponding to a measurable Clight subtrace.
2515 *)
2516
2517definition clight_normal : Clight_state → bool ≝
2518λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2519
2520definition cminor_normal : Cminor_state → bool ≝
2521λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2522
2523axiom clight_cminor_normal :
2524  ∀INV:clight_cminor_inv.
2525  ∀s1,s1',s2,tr.
2526  clight_cminor_rel INV s1 s1' →
2527  clight_normal s1 →
2528  ¬ Clight_labelled s1 →
2529  ∃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〉) →
2530  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2531    tr = tr' ∧
2532    clight_cminor_rel INV s2 s2'
2533  ).
2534
2535axiom clight_cminor_call_return :
2536  ∀INV:clight_cminor_inv.
2537  ∀s1,s1',s2,tr.
2538  clight_cminor_rel INV s1 s1' →
2539  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2540  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2541  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2542    tr = tr' ∧
2543    clight_cminor_rel INV s2 s2'
2544  ).
2545
2546axiom clight_cminor_cost :
2547  ∀INV:clight_cminor_inv.
2548  ∀s1,s1',s2,tr.
2549  clight_cminor_rel INV s1 s1' →
2550  Clight_labelled s1 →
2551  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2552  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2553    tr = tr' ∧
2554    clight_cminor_rel INV s2 s2'
2555  ).
2556
Note: See TracBrowser for help on using the repository browser.