source: src/Clight/toCminorCorrectnessExpr.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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