source: src/Clight/toCminorCorrectnessExpr.ma @ 2896

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

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

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