source: src/Clight/toCminorCorrectnessExpr.ma @ 3178

Last change on this file since 3178 was 3176, checked in by mckinna, 6 years ago

simplified dependencies

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