source: src/Clight/toCminorCorrectnessExpr.ma @ 2768

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

Add some more constraints in clight_cminor_data.

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