source: src/Clight/toCminorCorrectnessExpr.ma @ 2668

Last change on this file since 2668 was 2667, checked in by garnier, 8 years ago

Clight to Cminor, statements: some cases down. Subset of the simulation relation defined and seems to work.
Some cosmetic changes in toCminorCorrectnessExpr in order to clarify things in toCminorCorrectness.

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