source: src/Clight/toCminorCorrectness.ma @ 2569

Last change on this file since 2569 was 2569, checked in by campbell, 7 years ago

Fix Clight semantics for ptr + char. (Compiler works anyway.)

File size: 90.6 KB
Line 
1include "Clight/toCminor.ma".
2
3(* When we characterise the local Clight variables, those that are stack
4   allocated are given disjoint regions of the stack. *)
5
6lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7  characterise_vars globals f = 〈vartypes, stacksize〉 →
8  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9  ∀id',n',ty'. id ≠ id' →
10  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13whd in ⊢ (??%? → ?);
14generalize in match vartypes; -vartypes
15generalize in match stacksize; -stacksize
16elim (args@vars)
17[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18  elim globals in L;
19  [ normalize #L destruct
20  | * * #id' #r #ty' #tl #IH
21    whd in match (foldr ?????);
22    #L cases (lookup_add_cases ??????? L)
23    [ * #E1 #E2 destruct
24    | @IH
25    ]
26  ]
27| * #id1 #ty1 #tl #IH #stacksize #vartypes
28  whd in match (foldr ?????);
29  (* Avoid writing out the definition again *)
30  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31  lapply (refl ? ih) whd in match ih; -ih
32  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33  #vartypes' #stack' #FOLD #IH
34  whd in ⊢ (??(match % with [_⇒?])? → ?);
35  cases (orb ??)
36  #CHAR whd in CHAR:(??%?); destruct
37  #L cases (lookup_add_cases ??????? L)
38  [ 1,3: * #E1 #E2 destruct
39    #id' #n' #ty' #NE >lookup_add_miss /2/
40    #L' %1 -L -IH
41    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42    generalize in match stack'; -stack'
43    elim tl
44    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45      elim globals in L';
46      [ normalize #E destruct
47      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48        #L cases (lookup_add_cases ??????? L)
49        [ * #E1 #E2 destruct
50        | @IH
51        ]
52      ]
53    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55      #vartypes2 #stack2 #IH
56      whd in ⊢ (??%? → ?);
57      cases (orb ??)
58      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59        [ * #E1 #E2 destruct //
60        | #L'' lapply (IH ?? (refl ??) L'') /2/
61        ]
62      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63        [ * #E1 #E2 destruct
64        | #L'' lapply (IH ?? (refl ??) L'') /2/
65        ]
66      ]
67    ]
68  | -L #L #id' #n' #ty' #NE #L'
69    cases (lookup_add_cases ??????? L')
70    [ * #E1 #E2 destruct
71      %2 -IH -L'
72      generalize in match vartypes' in FOLD L; -vartypes'
73      generalize in match stack'; -stack'
74      elim tl
75      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76        elim globals in L;
77        [ normalize #E destruct
78        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79          #L cases (lookup_add_cases ??????? L)
80          [ * #E1 #E2 destruct
81          | @IH
82          ]
83        ]
84      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86        #vartypes2 #stack2 #IH
87        whd in ⊢ (??%? → ?);
88        cases (orb ??)
89        #E whd in E:(??%?); destruct
90        #L cases (lookup_add_cases ??????? L)
91        [ 1,3: * #E1 #E2 destruct //
92        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93        ]
94      ]
95    | @(IH … (refl ??) L … NE)
96    ]
97  | -L #L #id' #n' #ty' #NE #L'
98    cases (lookup_add_cases ??????? L')
99    [ * #E1 #E2 destruct
100    | @(IH … (refl ??) L … NE)
101    ]
102  ]
103] qed.
104
105(* And everything is in the stack frame. *)
106
107lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108  characterise_vars globals f = 〈vartypes, stacksize〉 →
109  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110  n + sizeof ty ≤ stacksize.
111#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112elim (args@vars)
113[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114  whd in FOLD:(??%?); destruct elim globals in L;
115  [ #E normalize in E; destruct
116  | * * #id' #r' #ty' #tl' #IH
117    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118    [ * #E1 #E2 destruct
119    | @IH
120    ]
121  ]
122| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124  #vartypes' #stackspace' #IH
125  whd in ⊢ (??(match % with [_⇒?])? → ?);
126  cases (orb ??) whd in ⊢ (??%? → ?);
127  #E destruct #L cases (lookup_add_cases ??????? L)
128  [ 1,3: * #E1 #E2 destruct //
129  | 2,4: #L' lapply (IH … (refl ??) L') /2/
130  ]
131] qed.
132
133(* Local variables show up in the variable characterisation as local. *)
134
135lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
136  characterise_vars globals f = 〈vartypes, stacksize〉 →
137  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
138  ∃t. local_id vartypes id t.
139#globals * #ret #args #vars #body
140whd in match (characterise_vars ??); elim (args@vars)
141[ #vartypes #stacksize #id #_ *
142| * #hd #ty #tl #IH
143  #vartypes #stacksize #id
144  whd in match (foldr ?????);
145  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
146  #vartypes' #stackspace' #IH
147  whd in ⊢ (??(match % with [_⇒?])? → ?);
148  cases (orb ??)
149  #E whd in E:(??%?); destruct *
150  [ 1,3: #E destruct %{(typ_of_type ty)}
151    whd whd in match (lookup' ??); >lookup_add_hit //
152  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
153    cases (identifier_eq ? id hd)
154    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
155    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
156    ]
157  ]
158] qed.
159
160(* Put knowledge that Globals are global into a more useful form than the
161   one used for the invariant. *)
162
163lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
164  characterise_vars globals f = 〈vartypes, stacksize〉 →
165  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
166  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
167  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
168#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
169cases (characterise_vars_src … CHAR id ?)
170[ * #r' * #ty' >L
171  * #E1 destruct (E1) #EX
172  %
173  [ @EX
174  | % #EX' cases (characterise_vars_localid … CHAR EX')
175    #ty' whd in ⊢ (% → ?); >L *
176  ]
177| * #ty' whd in ⊢ (% → ?); >L *
178| whd >(opt_eq_from_res ???? L) % #E destruct
179] qed.
180
181
182(* Show how the global environments match up. *)
183
184lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
185  map_partial_All A B P f l H = OK ? l' →
186  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
187#A #B #P #f #l
188elim l
189[ #H #l' #MAP normalize in MAP; destruct //
190| #h #t #IH * #p #H #l'
191  whd in ⊢ (??%? → ?);
192  lapply (refl ? (f h p)) whd in match (proj1 ???);
193  cases (f h p) in ⊢ (???% → %);
194  [ #b #E #MAP cases (bind_inversion ????? MAP)
195    #tl' * #MAP' #E' normalize in E'; destruct
196    % [ %{p} @E | @IH [ @H | @MAP' ] ]
197  | #m #_ #X normalize in X; destruct
198  ]
199] qed.
200 
201
202definition clight_cminor_matching : clight_program → matching ≝
203λp.
204  let tmpuniverse ≝ universe_for_program p in
205  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
206  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
207  let globals ≝ fun_globals @ var_globals in
208  mk_matching
209    ?? (list init_data × type) (list init_data)
210    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
211    (λv,w. \fst v = w).
212
213lemma clight_to_cminor_varnames : ∀p,p'.
214  clight_to_cminor p = OK ? p' →
215  prog_var_names … p = prog_var_names … p'.
216* #vars #fns #main * #vars' #fns' #main'
217#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
218whd in E:(??%%); destruct
219-MAP normalize
220elim vars
221[ //
222| * * #id #r * #d #t #tl #IH normalize >IH //
223] qed.
224
225
226lemma clight_to_cminor_matches : ∀p,p'.
227  clight_to_cminor p = OK ? p' →
228  match_program (clight_cminor_matching p) p p'.
229* #vars #fns #main * #vars' #fns' #main'
230#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
231whd in E:(??%%); destruct
232%
233[ -MAP whd in match (m_V ?); whd in match (m_W ?);
234  elim vars
235  [ //
236  | * * #id #r * #init #ty #tl #IH %
237    [ % //
238    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
239    ]
240  ]
241| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
242  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
243  normalize in E; destruct
244  <(clight_to_cminor_varnames … TO)
245  % whd
246  % [2: % [2: @TRANSF | skip ] | skip ]
247| %
248] qed.
249
250include "Clight/Cexec.ma".
251include "Clight/abstract.ma".
252include "Cminor/abstract.ma".
253
254(* Invariants used in simulation *)
255
256record clight_cminor_inv : Type[0] ≝ {
257  globals : list (ident × region × type);
258  ge_cl : genv_t clight_fundef;
259  ge_cm : genv_t (fundef internal_function);
260  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
261  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
262    ∃tmp_u,f',H1,H2.
263      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
264      find_funct … ge_cm v = Some ? f'
265}.
266
267include "Clight/CexecInd.ma".
268include "Clight/frontend_misc.ma".
269include "Clight/memoryInjections.ma".
270
271(* Perhaps we will have to be more precise on what is allocated, etc.
272   cf [exec_alloc_variables]. For now this is conveniently hidden in
273   the [value_eq E v v'] *)
274definition memory_matching ≝
275  λE:embedding.
276  λm,m':mem.
277  λen:cl_env.
278  λvenv:cm_env.
279  λcminv:clight_cminor_inv.
280  λsp:block.
281  λvars:var_types.
282  ∀id.
283    match lookup SymbolTag ? en id with
284    [ None ⇒
285      match find_symbol ? (ge_cl cminv) id with
286      [ None ⇒ True
287      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
288      ]
289    | Some cl_blo ⇒
290         match lookup ?? vars id with
291         [ Some kind ⇒
292            let 〈vtype, type〉 ≝ kind in
293            match vtype with
294            [ Stack n ⇒
295              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
296            | Local ⇒
297              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
298                   ∃v'. lookup ?? venv id = Some ? v' ∧
299                        value_eq E v v'
300            | _ ⇒ False ]
301        | None ⇒ False ]
302    ].
303             
304lemma type_should_eq_inversion :
305  ∀ty1,ty2,P,f,res.
306    type_should_eq ty1 ty2 P f = OK ? res →
307    ty1 = ty2 ∧ f ≃ res.
308#ty1 #ty2 #P #f #res normalize
309cases (type_eq_dec ty1 ty2) normalize nodelta
310[ 2: #Hneq #Habsurd destruct ]
311#Heq #Heq2 @conj try assumption
312destruct (Heq2) cases Heq normalize nodelta
313@eq_to_jmeq @refl
314qed.
315
316lemma typ_should_eq_inversion :
317  ∀ty1,ty2,P,a,x.
318    typ_should_eq ty1 ty2 P a = OK ? x →
319    ty1 = ty2 ∧ a ≃ x.
320* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
321[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
322| 3: cases sz cases sg #P #A #x normalize #H destruct
323| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
324cases sz cases sz2 cases sg cases sg2
325#P #a #x #H normalize in H:(??%?); destruct (H)
326try @conj try @refl try @refl_jmeq
327qed.
328
329lemma load_value_of_type_by_ref :
330  ∀ty,m,b,off,val.
331    load_value_of_type ty m b off = Some ? val →
332    typ_of_type ty ≃ ASTptr →
333    access_mode ty ≃ By_reference →
334    val = Vptr (mk_pointer b off).
335*
336[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
337| #structname #fieldspec | #unionname #fieldspec | #id ]
338#m #b #off #val
339[ 1,6,7: normalize #Habsurd destruct (Habsurd)
340| 4,5: normalize #Heq #_ #_ destruct @refl
341| 2: #_ normalize #Heq destruct
342| *: #Hload normalize #_ #H
343      lapply (jmeq_to_eq ??? H) #Heq destruct
344] qed.
345
346lemma load_value_of_type_by_value :
347  ∀ty,m,b,off,val.
348  access_mode ty = By_value (typ_of_type ty) →
349  load_value_of_type ty m b off = Some ? val →
350  loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
351
352[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
353| #structname #fieldspec | #unionname #fieldspec | #id ]
354#m #b #off #val
355normalize in match (access_mode ?);
356[ 1,4,5,6,7: #Habsurd destruct ]
357#_
358#H @H
359qed.
360
361include "Clight/CexecSound.ma".
362
363lemma lookup_exec_alloc :
364  ∀source_variables, initial_env, env, var_id, clb, m, m'.
365  lookup ?? env var_id = Some ? clb →
366  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
367  lookup ?? initial_env var_id = Some ? clb ∨
368  Exists ? (λx. \fst x = var_id) source_variables.
369#source_variables
370elim source_variables
371[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
372     destruct (Hexec_alloc) %1 @Hlookup
373| 2: * #id #ty #tail #Hind
374     #init_env #env #var #clb #m #m' #Hlookup     
375     whd in ⊢ (??%? → ?);
376     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
377     #Hexec_alloc
378     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
379     [ 1: destruct (Heq) %2 %1 @refl ]
380     cases (Hind … Hlookup Hexec_alloc)
381     [ @cthulhu (* standard reasoning on positive_maps. check lib. *)
382     | #Hexists %2 %2 @Hexists ]
383] qed.
384
385lemma characterise_vars_lookup_local :
386  ∀globals,f,vartypes,stacksize,id,clb,env.
387   characterise_vars globals f = 〈vartypes, stacksize〉 →
388   lookup ?? env id = Some ? clb →
389   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
390   ∃t. local_id vartypes id t.
391#globals #f #vartypes #stacksize #id #clb #env
392#Hchar #Hlookup * #m * #m' #Hexec
393cases (lookup_exec_alloc … Hlookup Hexec)
394[ normalize in ⊢ (% → ?); #Heq destruct
395| @(characterise_vars_localid … Hchar) ]
396qed.
397
398
399lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
400  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
401  lookup ?? env' var_id = None ? →
402  lookup ?? env var_id = None ? ∧
403  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
404#vars elim vars
405[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
406  #H @conj try @H % //
407| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
408  whd in ⊢ ((??%?) → ? → ?);
409  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
410  normalize nodelta #Hexec #Hlookup
411  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
412  cases env #env cases id' #id' cases var #var normalize
413  @(eqb_elim … id' var)
414  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
415       #Heq <Heq @conj try @Hlookup' % *
416       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
417       | cases Hexists' #H @H ]
418  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
419       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
420       >H1 in Hlookup'; #Heq destruct
421  ]
422] qed.
423
424lemma variable_not_in_env_but_in_vartypes_is_global :
425  ∀env,env',f,vars,stacksize,globals,var_id.
426  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
427  characterise_vars globals f =〈vars,stacksize〉 →
428  lookup ?? env' var_id = None ? →       
429  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
430  ∃r.allocty = Global r.
431#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
432#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
433lapply (characterise_vars_src … Hcharacterise var_id ?)
434[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
435 #Hlookup >Hlookup #_ #Habsurd destruct ]
436*
437[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
438     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
439* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
440@(match allocty
441  return λx. allocty = x → ?
442  with
443  [ Global r ⇒ λ_. ?
444  | Stack st' ⇒ λHalloc. ?
445  | Local ⇒ λHalloc. ?
446  ] (refl ? allocty))
447[ @False_ind ] normalize nodelta
448#Heq_typ
449(* Halloc is in contradiction with Hlookup_fail *)
450lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
451* #Hlookup' #Hnot_exists
452lapply (characterise_vars_all … Hcharacterise var_id t ?)
453[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
454#Hexists @False_ind
455cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
456[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
457       * #id' #ty' #tl #Hind *
458       [ 1,3: * #Heq #_ %1 @Heq
459       | *: #H %2 @Hind @H ] ]
460#H cases Hnot_exists #H' @H' @H
461qed.
462
463
464lemma translate_notbool_to_cminor :
465  ∀t,sg,arg.
466  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
467  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
468        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
469*
470[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
471| #structname #fieldspec | #unionname #fieldspec | #id ]
472normalize in match (typ_of_type ?);
473#sg #arg #cmop
474whd in ⊢ (??%% → ?); #Heq destruct (Heq)
475cases arg
476[ | #vsz #vi | | #vp
477| | #vsz #vi | | #vp
478| | #vsz #vi | | #vp
479| | #vsz #vi | | #vp
480| | #vsz #vi | | #vp
481| | #vsz #vi | | #vp
482| | #vsz #vi | | #vp
483| | #vsz #vi | | #vp ]
484#res
485whd in ⊢ ((??%?) → ?);
486#Heq
487[ 6,11,12: | *: destruct (Heq) ]
488[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
489| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
490     #H normalize nodelta #Heq destruct
491     whd in match (eval_unop ????);
492     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
493] qed.
494
495lemma translate_notint_to_cminor :
496  ∀t,t',arg.
497  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
498  ∀res. sem_unary_operation Onotint arg t = Some ? res →
499        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
500#ty *
501[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
502#sz #sg #arg #cmop
503whd in match (translate_unop ???);
504@(match typ_eq (ASTint sz sg) (typ_of_type ty)
505  with
506  [ inl H ⇒ ?
507  | inr H ⇒ ? ])
508normalize nodelta
509[ 2: #Heq destruct ]
510lapply H -H
511lapply cmop -cmop
512cases ty
513[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
514| #structname #fieldspec | #unionname #fieldspec | #id ]
515normalize nodelta
516#cmop normalize in match (typ_of_type ?); #H destruct
517#H' normalize in H';
518destruct (H')
519#res
520whd in match (sem_unary_operation ???);
521cases arg
522[ | #vsz #vi | | #vp
523| | #vsz #vi | | #vp
524| | #vsz #vi | | #vp
525| | #vsz #vi | | #vp ]
526whd in match (sem_notint ?);
527#H destruct (H) @refl
528qed.
529
530
531lemma translate_negint_to_cminor :
532  ∀t,t',arg.
533  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
534  ∀res. sem_unary_operation Oneg arg t = Some ? res →
535        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
536#ty *
537[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
538#sz #sg #arg #cmop
539whd in match (translate_unop ???);
540@(match typ_eq (ASTint sz sg) (typ_of_type ty)
541  with
542  [ inl H ⇒ ?
543  | inr H ⇒ ? ])
544normalize nodelta
545[ 2: #Heq destruct ]
546lapply H -H
547lapply cmop -cmop
548cases ty
549[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
550| #structname #fieldspec | #unionname #fieldspec | #id ]
551normalize nodelta
552#cmop normalize in match (typ_of_type ?); #H destruct
553#H' normalize in H';
554destruct (H')
555#res
556whd in match (sem_unary_operation ???);
557cases arg
558[ | #vsz #vi | | #vp
559| | #vsz #vi | | #vp
560| | #vsz #vi | | #vp
561| | #vsz #vi | | #vp ]
562whd in match (sem_neg ??);
563#H destruct (H)
564whd in match (eval_unop ????);
565cases (eq_intsize sz' vsz) in H; normalize nodelta
566#H destruct @refl
567qed.
568
569
570lemma translate_unop :
571  ∀ty,sg,op,cmop.
572  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
573  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
574            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
575#ty #sg * #cmop #Htranslate #arg
576[ @translate_notbool_to_cminor assumption
577| @translate_notint_to_cminor assumption
578| @translate_negint_to_cminor assumption ]
579qed.
580
581lemma classify_add_inversion :
582  ∀ty1,ty2.
583    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
584    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
585    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
586    (classify_add ty1 ty2 = add_default ty1 ty2).
587#ty1 #ty2
588cases (classify_add ty1 ty2)
589[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
590| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
591| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
592| #tya #tyb %2 @refl ]
593qed.
594
595lemma classify_aop_inversion :
596  ∀ty1,ty2.
597    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
598    classify_aop ty1 ty2 = aop_default ty1 ty2.
599#ty1 #ty2
600cases (classify_aop ty1 ty2)
601[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
602| #ty #ty' %2 @refl ]
603qed.
604
605lemma sem_add_ip_inversion :
606  ∀sz,sg,ty',optlen.
607  ∀v1,v2,res.
608  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
609  ∃sz',i. v1 = Vint sz' i ∧
610      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
611       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
612#tsz #tsg #ty' * [ | #n ]
613*
614[ | #sz' #i' | | #p'
615| | #sz' #i' | | #p' ]
616#v2 #res
617whd in ⊢ ((??%?) → ?);
618#H destruct
619cases v2 in H;
620[ | #sz2' #i2' | | #p2'
621| | #sz2' #i2' | | #p2' ] normalize nodelta
622#H destruct
623[ 1,3:
624  lapply H -H
625  @(eq_bv_elim … i' (zero ?)) normalize nodelta
626  #Hi #Heq destruct (Heq)
627  %{sz'} %{(zero ?)} @conj destruct try @refl
628  %2 @conj try @conj try @refl
629| *: %{sz'} %{i'} @conj try @refl
630  %1 %{p2'} @conj try @refl
631] qed.
632
633(* symmetric of the upper one *)
634lemma sem_add_pi_inversion :
635  ∀sz,sg,ty',optlen.
636  ∀v1,v2,res.
637  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
638  ∃sz',i. v2 = Vint sz' i ∧
639      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
640       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
641#tsz #tsg #ty' * [ | #n ]
642*
643[ | #sz' #i' | | #p'
644| | #sz' #i' | | #p' ]
645#v2 #res
646whd in ⊢ ((??%?) → ?);
647#H destruct
648cases v2 in H; normalize nodelta
649[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
650#H destruct
651[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
652  %{p'} @conj try @refl
653| *: lapply H -H
654  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
655  #Hi #Heq destruct (Heq)
656  %{sz2'} %{(zero ?)} @conj destruct try @refl
657  %2 @conj try @conj try @refl
658] qed.
659
660(* Know that addition on integers gives an integer. Notice that there is no correlation
661   between the size in the types and the size of the integer values. *)
662lemma sem_add_ii_inversion :
663  ∀sz,sg.
664  ∀v1,v2,res.
665  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
666  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
667              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
668#sz #sg
669*
670[ | #sz' #i' | | #p' ]
671#v2 #res
672whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
673cases sz cases sg normalize nodelta
674#H destruct
675cases v2 in H; normalize nodelta
676#H1 destruct
677#H2 destruct #Heq %{sz'} lapply Heq -Heq
678cases sz' in i'; #i' 
679whd in match (intsize_eq_elim ???????);
680cases H1 in H2; #j' normalize nodelta
681#Heq destruct (Heq)
682%{i'} %{j'} @conj try @conj try @conj try @refl
683qed.
684
685lemma sem_mul_inversion :
686  ∀sz,sg.
687  ∀v1,v2,res.
688  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
689  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
690              res = Vint sz' (short_multiplication ? i1 i2).
691#sz #sg *
692[ | #sz' #i' | | #p' ]
693#v2 #res
694whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
695cases sz cases sg normalize nodelta
696#H destruct
697cases v2 in H; normalize nodelta
698#H1 destruct
699#H2 destruct #Heq %{sz'} lapply Heq -Heq
700cases sz' in i'; #i' 
701whd in match (intsize_eq_elim ???????);
702cases H1 in H2; #j' normalize nodelta
703#Heq destruct (Heq)
704%{i'} %{j'} @conj try @conj try @conj try @refl
705qed.
706
707
708lemma sem_div_inversion_s :
709  ∀sz.
710  ∀v1,v2,res.
711  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
712  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
713              match division_s ? i1 i2 with
714              [ Some q ⇒  res =  (Vint sz' q)
715              | None ⇒ False ].
716#sz *
717[ | #sz' #i' | | #p' ]
718#v2 #res
719whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
720>type_eq_dec_true normalize nodelta
721#H destruct
722cases v2 in H; normalize nodelta
723[ | #sz2' #i2' | | #p2' ]
724#Heq destruct
725%{sz'}
726lapply Heq -Heq
727cases sz' in i'; #i' 
728whd in match (intsize_eq_elim ???????);
729cases sz2' in i2'; #i2' normalize nodelta
730whd in match (option_map ????); #Hdiv destruct
731%{i'} %{i2'} @conj try @conj try @conj try @refl
732cases (division_s ???) in Hdiv;
733[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
734qed.
735
736lemma sem_div_inversion_u :
737  ∀sz.
738  ∀v1,v2,res.
739  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
740  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
741              match division_u ? i1 i2 with
742              [ Some q ⇒  res =  (Vint sz' q)
743              | None ⇒ False ].
744#sz *
745[ | #sz' #i' | | #p' ]
746#v2 #res
747whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
748>type_eq_dec_true normalize nodelta
749#H destruct
750cases v2 in H; normalize nodelta
751[ | #sz2' #i2' | | #p2' ]
752#Heq destruct
753%{sz'}
754lapply Heq -Heq
755cases sz' in i'; #i' 
756whd in match (intsize_eq_elim ???????);
757cases sz2' in i2'; #i2' normalize nodelta
758whd in match (option_map ????); #Hdiv destruct
759%{i'} %{i2'} @conj try @conj try @conj try @refl
760cases (division_u ???) in Hdiv;
761[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
762qed.
763
764lemma expr_vars_fix_ptr_type :
765  ∀ty',optlen.
766  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
767  ∀P.
768   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
769   expr_vars
770    (typ_of_type
771        match optlen 
772        in option 
773        return λ_:(option ℕ).type with 
774        [None⇒Tpointer ty'
775        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
776#ty' * normalize
777[ 2: #n ]
778#e #P
779@expr_vars_mp //
780qed.
781
782(* This lemma is just noise. *)
783lemma eval_expr_rewrite_aux :
784  ∀genv.
785  ∀optlen.
786  ∀ty'.
787  ∀e.
788  ∀cm_env.
789  ∀H.
790  ∀sp.
791  ∀m.
792  ∀res.
793  (eval_expr genv
794             (typ_of_type
795                 match optlen in option return λ_:(option ℕ).type with 
796                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
797             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 →
798   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
799#genv * [ 2: #n ] normalize nodelta
800#ty' normalize in match (typ_of_type ?);
801#e #cm_env whd in match (fix_ptr_type ???);
802#H #sp #m #res #H @H
803qed.
804
805
806(* TODOs : there are some glitches between clight and cminor :
807 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
808      in the shortcut case, the cminor code returns directly the outcome of the
809      evaluated expr, with a possibly different size.
810   2) another glitch is for the integer/pointer additions: Clight always performs
811      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
812      the sign of i, producing either a sign extension or a zero extension.
813 *)
814lemma eval_expr_sim :
815  ∀(inv:clight_cminor_inv).
816  ∀(f:function).
817  ∀(vars:var_types).
818  ∀stacksize.
819  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
820  ∀(cl_env:cl_env).
821  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
822  ∀(cl_m:mem).
823  ∀(cm_env:cm_env).
824  ∀(sp:block).
825  ∀(cm_m:mem).
826  ∀E:embedding.
827  ∀minj:memory_inj E cl_m cm_m.
828  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
829  (* clight expr to cminor expr *)
830  (∀(e:expr).
831   ∀(e':CMexpr (typ_of_type (typeof e))).
832   ∀Hexpr_vars.
833   translate_expr vars e = OK ? («e', Hexpr_vars») →
834   ∀cl_val,trace,Hyp_present.
835   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
836   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
837            value_eq E cl_val cm_val) ∧
838   (* clight /lvalue/ to cminor /expr/ *)
839  (∀ed,ty.
840   ∀(e':CMexpr ASTptr).
841   ∀Hexpr_vars.
842   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
843   ∀cl_blo,cl_off,trace,Hyp_present.
844   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
845   ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
846            value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
847#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
848@expr_lvalue_ind_combined
849[ 7: (* binary ops *)
850     #ty
851     #op #e1 #e2
852     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
853     cases (bind_inversion ????? Htranslate) -Htranslate
854     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
855     cases (bind_inversion ????? Htranslate) -Htranslate
856     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
857     whd in ⊢ ((??%?) → ?);
858     #Htranslate_binop
859     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
860     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
861     #cl_val #trace #Hyp_present #Hexec
862     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
863     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
864     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
865     lapply Hyp_present -Hyp_present
866     lapply Htranslate_lhs -Htranslate_lhs
867     lapply Htranslate_rhs -Htranslate_rhs
868     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
869     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
870     lapply Hexec -Hexec
871     lapply Htranslated_binop -Htranslated_binop
872     lapply rhs -rhs lapply lhs -lhs
873     (* end of dump *)
874     cases op
875     whd in ⊢ (? → ? → (??%?) → ?);
876     [ 1: (* add *)
877       lapply (classify_add_inversion (typeof e1) (typeof e2))
878       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
879       (* trying to factorise as much stuff as possible ... *)
880       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
881       * [ 1: * ]
882       [ 1: * #sz * #sg * *
883       | 2: * #optlen * #ty' * #sz * #sg * *
884       | 3: * #optlen * #sz * #sg * #ty' * * ]
885       whd in match (typeof ?) in ⊢ (% → % → ?);
886       #Htypeof_e1 #Htypeof_e2
887       >Htypeof_e1 >Htypeof_e2
888       #Hclassify
889       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
890       normalize nodelta
891       whd in match (typeof ?) in ⊢ (% → % → %);
892       whd in match (typ_of_type (Tint ??));
893       #lhs #rhs #Htyp_should_eq
894       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
895       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
896       -Htyp_should_eq
897       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
898       <Heq_e' -Heq_e'
899       #Hexec
900       #Hexpr_vars_rhs #Hexpr_vars_lhs
901       #Htranslate_rhs #Htranslate_lhs
902       * [ #Hyp_present_lhs #Hyp_present_rhs
903         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
904         | #Hyp_present_rhs * #Hyp_present_lhs #Hyp_present_cst  ]
905       whd in match (typeof ?);
906       #Hind_rhs #Hind_lhs
907       cases (bind_inversion ????? Hexec) -Hexec
908       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
909       cases (bind_inversion ????? Hexec) -Hexec
910       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
911       cases (bind_inversion ????? Hexec) -Hexec
912       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
913       lapply (opt_to_res_inversion ???? Hsem) -Hsem
914       whd in match (typeof ?); whd in match (typeof ?);
915       #Hsem_binary
916       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
917       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
918       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
919       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
920       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
921       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
922       whd in match (eval_expr ???????);
923       whd in match (proj1 ???);
924       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
925       [ 1,2: >Heval_lhs normalize nodelta
926              whd in match (eval_expr ???????);
927              whd in match (eval_expr ???????);
928              >Heval_rhs normalize nodelta
929              whd in match (m_bind ?????);
930       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
931            whd in match (eval_expr ???????);
932            whd in match (eval_expr ???????);
933            >Heval_lhs normalize nodelta
934       ]
935       whd in match (proj1 ???); whd in match (proj2 ???);
936       [ 2: (* standard int/int addition. *)
937            whd in match (eval_binop ???????);
938            whd in Hsem_binary:(??%?);
939            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
940            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
941            cases (sem_add_ii_inversion … Hsem_binary_translated)
942            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
943            #Hcm_lhs #Hcm_rhs #Hcm_val
944            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
945            >intsize_eq_elim_true normalize nodelta
946            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
947            @conj try @refl lapply Hsem_binary_translated
948            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
949            >inttyp_eq_elim_true' normalize nodelta
950            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
951       | *: (* pointer/int int/pointer addition *)
952            whd in Hsem_binary:(??%?);
953            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
954            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
955            [ 1: lapply (sem_add_pi_inversion … Hsem_binary_translated)
956                 * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
957                 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
958                 | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
959                 destruct
960                 whd in match (eval_unop ????);
961                 @(match sg
962                   return λs. sg = s → ?
963                   with
964                   [ Unsigned ⇒ λHsg. ?
965                   | Signed ⇒ λHsg. ?
966                   ] (refl ??)) normalize nodelta
967                   whd in match (eval_binop ???????);
968                   whd in match (m_bind ?????);
969                   [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
970                                   (short_multiplication (bitsize_of_intsize I16)
971                                   (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
972                                   (repr I16 (sizeof ty')))))}
973                   | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
974                                   (short_multiplication (bitsize_of_intsize I16)
975                                   (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
976                                   (repr I16 (sizeof ty')))))} ]
977                   [ 1,2: @conj whd in match (E0); whd in match (Eapp trace_rhs ?);
978                          >(append_nil … trace_rhs) try @refl
979                          @(value_eq_triangle_diagram … Hvalue_eq_res)
980                          whd in match (shift_pointer_n ????);
981                          whd in match (shift_offset_n ????);
982                          >commutative_short_multiplication
983                          whd in match (shift_pointer ???);
984                          whd in match (shift_offset ???);
985                          @cthulhu (* cf problem description at top of lemma. *)
986                   | 3: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
987                        >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
988                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
989                        normalize >append_nil try @refl
990                   | 4: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
991                        >(short_multiplication_zero 16 (repr I16 (sizeof ty')))
992                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
993                        normalize >append_nil try @refl ]
994            | 2: (* integer/pointer add: symmetric to the case above. *) @cthulhu ]
995       ]
996     | 2: (* subtraction cases: identical to add *) @cthulhu
997     | 3: (* mul *)
998       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
999       [ 2,4: #Hclassify >Hclassify normalize nodelta
1000            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1001       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1002       whd in match (typeof ?); #e'
1003       * #sz * #sg * *
1004       whd in match (typeof ?) in ⊢ (% → % → ?);
1005       #Htypeof_e1 #Htypeof_e2
1006       >Htypeof_e1 >Htypeof_e2
1007       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1008       #Hclassify
1009       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1010       normalize nodelta
1011       whd in match (typ_of_type (Tint ??));
1012       #lhs #rhs #Htyp_should_eq
1013       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1014       -Htyp_should_eq
1015       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1016       <Heq_e' -Heq_e'
1017       #Hexec
1018       #Hexpr_vars_rhs #Hexpr_vars_lhs
1019       #Htranslate_rhs #Htranslate_lhs
1020       * #Hyp_present_lhs #Hyp_present_rhs
1021       #Hind_rhs #Hind_lhs
1022       cases (bind_inversion ????? Hexec) -Hexec
1023       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1024       cases (bind_inversion ????? Hexec) -Hexec
1025       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1026       cases (bind_inversion ????? Hexec) -Hexec
1027       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1028       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1029       whd in match (typeof ?); whd in match (typeof ?);
1030       #Hsem_binary
1031       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1032       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1033       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1034       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1035       whd in match (eval_expr ???????);
1036       whd in match (proj1 ???);
1037       >Heval_lhs normalize nodelta
1038       >Heval_rhs normalize nodelta
1039       whd in match (m_bind ?????);
1040       whd in match (eval_binop ???????);
1041       whd in Hsem_binary:(??%?);
1042       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1043       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1044       cases (sem_mul_inversion … Hsem_binary)
1045       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1046       #Hcm_lhs #Hcm_rhs #Hcm_val
1047       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1048       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1049       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1050       >intsize_eq_elim_true normalize nodelta
1051       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1052       @conj try @refl
1053       whd in Hsem_binary:(??%?);     
1054       whd in match (classify_aop ??) in Hsem_binary:(??%?);
1055       >type_eq_dec_true in Hsem_binary; normalize nodelta
1056       >intsize_eq_elim_true #Heq destruct (Heq)
1057       %2
1058     | 4: (* div *)
1059       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1060       [ 2,4: #Hclassify >Hclassify normalize nodelta
1061            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1062       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1063       whd in match (typeof ?); #e'
1064       * #sz * * * *
1065       whd in match (typeof ?) in ⊢ (% → % → ?);
1066       #Htypeof_e1 #Htypeof_e2
1067       >Htypeof_e1 >Htypeof_e2
1068       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1069       #Hclassify
1070       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1071       normalize nodelta
1072       whd in match (typ_of_type (Tint ??));
1073       #lhs #rhs #Htyp_should_eq
1074       [ cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1075       | cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1076       -Htyp_should_eq
1077       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1078       <Heq_e' -Heq_e'
1079       #Hexec
1080       #Hexpr_vars_rhs #Hexpr_vars_lhs
1081       #Htranslate_rhs #Htranslate_lhs
1082       * #Hyp_present_lhs #Hyp_present_rhs
1083       #Hind_rhs #Hind_lhs
1084       cases (bind_inversion ????? Hexec) -Hexec
1085       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1086       cases (bind_inversion ????? Hexec) -Hexec
1087       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1088       cases (bind_inversion ????? Hexec) -Hexec
1089       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1090       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1091       whd in match (typeof ?); whd in match (typeof ?);
1092       #Hsem_binary
1093       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1094       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1095       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1096       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1097       whd in match (eval_expr ???????);
1098       whd in match (proj1 ???);
1099       >Heval_lhs normalize nodelta
1100       >Heval_rhs normalize nodelta
1101       whd in match (m_bind ?????);
1102       whd in match (eval_binop ???????);
1103       whd in Hsem_binary:(??%?);
1104       lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1105       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1106       [ cases (sem_div_inversion_s … Hsem_binary)
1107       | cases (sem_div_inversion_u … Hsem_binary) ]
1108       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1109       #Hcm_lhs #Hcm_rhs #Hcm_val
1110       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1111       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1112       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1113       >intsize_eq_elim_true normalize nodelta
1114       [ cases (division_s ???) in Hcm_val; normalize nodelta
1115         [ @False_ind
1116         | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ]
1117       | cases (division_u ???) in Hcm_val; normalize nodelta
1118         [ @False_ind
1119         | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ] ]
1120     | 5: (* mod *) @cthulhu
1121     | 6: (* and *) @cthulhu
1122     | 7: (* or *)  @cthulhu
1123     | 8: (* xor *) @cthulhu
1124     | 9: (* shl *) @cthulhu
1125     | 10: (* shr *) @cthulhu
1126     | 11: (* eq *) @cthulhu
1127     | 12: (* ne *) @cthulhu
1128     | 13: (* lt *) @cthulhu
1129     | 14: (* gt *) @cthulhu
1130     | 15: (* le *) @cthulhu
1131     | 16: (* ge *) @cthulhu ]
1132     
1133| 1: (* Integer constant *)
1134  #csz #ty cases ty
1135  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1136  | #structname #fieldspec | #unionname #fieldspec | #id ]
1137  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
1138  #val #trace #Hpresent #Hexec_cl
1139  whd in Htranslate:(??%?);
1140  [ 1,3,4,5,6,7,8: destruct ]
1141  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))))
1142  [ 2: * #H_err #H_neq_sz
1143       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1144       >Htranslate #Habsurd destruct (Habsurd) ]
1145  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1146  destruct (Heq_sz)
1147  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
1148  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
1149  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
1150| 2: *
1151  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
1152  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1153  try /2 by I/
1154  #ty whd in ⊢ (% → ?); #Hind
1155  whd in match (Plvalue ???);
1156  whd in match (typeof ?);
1157  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
1158  whd in Hexec:(??%?);
1159  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
1160  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
1161  whd in Hcl_success:(???%);
1162  [ 1: (* var case *)
1163       lapply Hcl_success -Hcl_success -Hind
1164       (* Peform case analysis on presence of variable in local Clight env.
1165        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
1166       @(match lookup SymbolTag block cl_env var_id
1167         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
1168         with
1169         [ None ⇒ λHcl_lookup. ?
1170         | Some loc ⇒ λHcl_lookup. ?
1171         ] (refl ? (lookup SymbolTag block cl_env var_id)))
1172       normalize nodelta
1173       [ 1: (* global case *)
1174            #Hlookup_global
1175            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
1176            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
1177            #Heq whd in Heq:(???%); destruct (Heq)
1178            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1179            * #var_id_alloctype * #var_id_type * #Heq
1180            cases (variable_not_in_env_but_in_vartypes_is_global …
1181                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
1182            #r #Heq' destruct (Heq') normalize nodelta
1183            lapply Hcl_load_success -Hcl_load_success
1184            lapply Hyp_present -Hyp_present
1185            lapply Hexpr_vars -Hexpr_vars
1186            lapply cm_expr -cm_expr inversion (access_mode ty)
1187            [ #typ_of_ty | | #typ_of_ty ]
1188            #Heq_typ_of_type #Heq_access_mode
1189            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1190            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1191            whd in match (eval_expr ???????);
1192            whd in match (eval_expr ???????);
1193            whd in match (eval_constant ????);
1194            <(eq_sym … inv) >Hfind_symbol normalize nodelta
1195            cases (bind_inversion ????? Hcl_load_success) #x *
1196            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
1197            lapply (opt_to_res_inversion ???? Hopt_to_res)
1198            #Hcl_load_success
1199            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1200                 @conj try @refl
1201                 whd in Hcm_load_success:(??%?);
1202                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
1203                 >(load_value_of_type_by_ref … Hcl_load_success)
1204                 try assumption %4
1205                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1206                 >Hfind_symbol normalize nodelta #Heq_embedding
1207                 whd in match (shift_offset ???);
1208                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
1209                 normalize nodelta @refl
1210            | 1: cut (access_mode ty=By_value (typ_of_type ty))
1211                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
1212                   lapply Heq_access_mode <Heqt // ] #Haccess
1213                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
1214                 #Hvalid_ptr
1215                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
1216                 [ whd in ⊢ (??%?);
1217                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1218                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
1219                 * #val' * #Hcm_load_success #Hvalue_eq
1220                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
1221                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
1222                 normalize %{val'} @conj try @refl assumption ]
1223       | 2: (* local case *)
1224            #Heq destruct (Heq)
1225            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1226            * #var_id_alloc_type * #var_id_type *
1227            generalize in match var_id_alloc_type; * normalize nodelta
1228            [ 1: #r #Hlookup_vartype
1229                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
1230                 * #typ whd in match (local_id ???);
1231                 >Hlookup_vartype normalize nodelta @False_ind
1232            | 2: (* Stack local *)
1233                 lapply Hcl_load_success -Hcl_load_success
1234                 lapply Hyp_present -Hyp_present
1235                 lapply Hexpr_vars -Hexpr_vars
1236                 lapply cm_expr -cm_expr inversion (access_mode ty)
1237                 [ #typ_of_ty | | #typ_of_ty ]
1238                 #Heq_typ_of_type #Heq_access_mode
1239                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
1240                 #stack_depth #Hlookup_vartype_success normalize nodelta
1241                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1242                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1243                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
1244                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1245                 >Hlookup' normalize nodelta #Hembedding_eq
1246                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1247                 #loaded_val * #Hload_val
1248                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1249                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1250                 #Hload_success whd in match (eval_expr ???????);
1251                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
1252                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
1253                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
1254                        >offset_plus_0 @refl ]
1255                 #Hpointer_translation
1256                 [ 2: (* By-ref *)
1257                      whd in Hload_success:(??%?);
1258                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
1259                      #Heq_val
1260                      >Heq_val
1261                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
1262                      @conj try @refl
1263                      %4 whd in match (shift_offset ???);
1264                      whd in match zero_offset;
1265                      >commutative_addition_n >addition_n_0 @Hpointer_translation
1266                 | 1: (* By value *)
1267                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
1268                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
1269                      [ @(load_by_value_success_valid_pointer … Hload_success)
1270                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
1271                      * #cm_val * #Hload_in_cm #Hvalue_eq
1272                      %{cm_val} @conj try assumption
1273                      lapply (load_value_of_type_by_value … Hload_in_cm)
1274                      [ lapply Heq_access_mode <Heq0 #Heq1
1275                        @(jmeq_to_eq ??? Heq1) ]
1276                      #Hloadv <Heq0
1277                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
1278                      >Hloadv @refl ]
1279            | 3: (* Register local variable *)
1280                 #Hlookup_eq
1281                 lapply (res_inversion ?????? Hlookup_eq)
1282                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1283                 #Htype_eq
1284                 cases (type_should_eq_inversion
1285                            var_id_type
1286                            ty
1287                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
1288                            … Htype_eq) -Htype_eq
1289                 (* Reverting all premises in order to perform type rewrite *)
1290                 #Htype_eq
1291                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
1292                 lapply Hcl_load_success -Hcl_load_success
1293                 lapply Hcl_lookup -Hcl_lookup
1294                 lapply Hyp_present -Hyp_present
1295                 lapply Hexpr_vars -Hexpr_vars
1296                 lapply cm_expr
1297                 destruct (Htype_eq)
1298                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
1299                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
1300                 destruct (Hexpr_eq)
1301                 whd in match (eval_expr ???????);
1302                 whd in match (lookup_present ?????);
1303                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1304                 >Hlookup' normalize nodelta #Hmatching
1305                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1306                 #loaded_val * #Hload_val
1307                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1308                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1309                 #Hload_success
1310                 cases (Hmatching … Hload_success) #val'
1311                 * #Hlookup_in_cm #Hvalue_eq %{val'}
1312                 cases Hyp_present
1313                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
1314                 (* seems ok *)
1315            ]
1316       ]
1317  | 2: lapply Hcl_success -Hcl_success
1318       lapply Htranslate_expr -Htranslate_expr
1319       lapply Hind -Hind cases ty1
1320       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1321       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1322       #Hind #Htranslate_expr #Hexec_cl
1323       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1324       * whd in match (typ_of_type ?); normalize nodelta
1325       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
1326       whd in ⊢ ((???%) → ?);
1327       [ 1,2,6,7: #Heq destruct (Heq) ]
1328       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
1329       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
1330       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
1331       [ 1,3,5,7: @cthulhu ]
1332       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
1333       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
1334       #Hexec_cl_ind #Hcl_ptr
1335       cut (∃ptr. cl_ptr = Vptr ptr)
1336       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
1337                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
1338       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
1339       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
1340       #Hind lapply (Hind (refl ??)) -Hind
1341       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
1342       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
1343       destruct (Hcm_ptr) #Hpointer_translation
1344       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
1345       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
1346       -Hopt_to_res
1347       lapply Hyp_present -Hyp_present
1348       lapply Hexpr_vars -Hexpr_vars
1349       lapply cm_expr -cm_expr
1350       inversion (access_mode ty)
1351       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
1352       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
1353       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1354       #Heq destruct (Heq)
1355       [ 1,2,3,4: (* By_value *)
1356           (* project Hcl_load_success in Cminor through memory_inj *)
1357           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
1358           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
1359           * #cm_val * #Hcm_load_success #Hvalue_eq
1360           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
1361           #Hloadv_cm
1362           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
1363           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
1364      | *: (* By reference *)
1365           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1366           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
1367           #Hval >Hval %4 assumption ]
1368  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
1369       lapply (refl ? (typeof e1))
1370       cases (typeof e1) in ⊢ ((???%) → %);
1371       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1372       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
1373       #Heq_typeof normalize nodelta
1374       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
1375       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
1376       normalize nodelta #Htranslate_expr
1377       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1378       * whd in match (typ_of_type ?); normalize nodelta
1379       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
1380       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
1381         #cm_field_off * #Hcm_field_off
1382       | lapply Htranslate_expr2 -Htranslate_expr2 ]
1383       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1384       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
1385       whd in Hexec_lvalue:(???%);
1386       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1387         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
1388       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1389       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1390       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
1391       [  (* Struct case *)
1392         lapply Hcl_load_value -Hcl_load_value
1393         lapply Hyp_present -Hyp_present
1394         lapply Hexpr_vars -Hexpr_vars
1395         lapply cm_expr -cm_expr
1396         lapply Hind -Hind
1397         cases ty
1398         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1399         | #structname #fieldspec | #unionname #fieldspec | #id ]
1400         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1401         normalize nodelta
1402         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1403         whd in match (eval_expr ???????);
1404         (* applying the arguments of the induction hypothesis progressively *)
1405         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
1406                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
1407         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
1408         lapply (Hind ?)
1409         [ 1,3,5,7,9:
1410            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1411            >Htranslate_expr_ind whd in match (m_bind ?????);
1412            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
1413         whd in Hoffset_eq:(???%); destruct (offset_eq)
1414         cut (cl_field_off = cm_field_off)
1415         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
1416           normalize #Heq destruct (Heq) @refl ]
1417         #Heq destruct (Heq)
1418         lapply (Hind cl_b cl_o trace ?)
1419         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
1420         lapply (Hind ?) -Hind
1421         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1422           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
1423           @Hoffset_eq ]
1424         * #cm_val' * #Heval_expr #Hvalue_eq
1425         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
1426         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
1427         [ 1,2,5: (* by-value *)
1428            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
1429            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1430            * #cm_val * #Hcm_load_value #Hvalue_eq
1431            lapply (load_value_of_type_by_value … Hcm_load_value)
1432            [ 1,3,5: @refl ]
1433            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
1434            try @refl try assumption
1435         | 3,4: (* by-ref *)
1436            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
1437            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1438            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
1439         ]
1440      | (* union case *)
1441         lapply Hcl_load_value -Hcl_load_value
1442         lapply Hyp_present -Hyp_present
1443         lapply Hexpr_vars -Hexpr_vars
1444         lapply cm_expr -cm_expr
1445         lapply Hind -Hind
1446         cases ty
1447         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1448         | #structname #fieldspec | #unionname #fieldspec | #id ]
1449         whd in match (typ_of_type ?); normalize nodelta
1450         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1451         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1452         [ 1,2,5: (* by-value *)
1453            whd in match (eval_expr ???????);
1454            lapply (Hind cm_expr_ind Hexpr_vars ?)
1455            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
1456            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1457            -Hind #Hind
1458            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
1459            whd in match (m_bind ?????); #Hind
1460            cases (Hind (refl ??)) -Hind
1461            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
1462            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
1463            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
1464            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
1465            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1466            * #cm_val * #Hcm_load_value #Hvalue_eq           
1467            lapply (load_value_of_type_by_value … Hcm_load_value)
1468            [ 1,3,5: @refl ]
1469            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
1470            try @refl assumption
1471         | 3,4:
1472            whd in Hexec_cl:(???%); destruct (Hexec_cl)
1473            lapply (Hind cm_expr Hexpr_vars)
1474            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
1475            lapply (Hind Htranslate_expr_ind) -Hind
1476            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1477            >Hexec_lvalue whd in match (m_bind ?????);
1478            #Hind cases (Hind … Hyp_present (refl ??))
1479            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
1480            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
1481            assumption ]
1482    ]
1483  ]
1484| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
1485     whd in Hexec_lvalue_var:(??%?);
1486     (* check whether var is local or global *)
1487     lapply (Hlocal_matching var)
1488     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
1489     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
1490     normalize nodelta
1491     [ 1: (* global *)
1492          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
1493          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
1494          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
1495          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
1496          #Hembed
1497          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1498          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
1499          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
1500          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1501          whd in match (eval_expr ???????);
1502          whd in match (eval_constant ????);
1503          <(eq_sym inv var) >Hfind_symbol normalize nodelta
1504          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1505          @conj try @refl %4 whd in match (pointer_translation ??);
1506          >Hembed normalize nodelta whd in match (shift_offset ???);
1507          >addition_n_0 @refl
1508     | 2: (* local *)
1509          #BL #Heq destruct (Heq) #_
1510          @(match (lookup ?? vars var)
1511            return λx. (lookup ?? vars var = x) → ?
1512            with
1513            [ None ⇒ ?
1514            | Some kind ⇒ ?
1515            ] (refl ??))
1516          normalize nodelta
1517          #Hlookup [ @False_ind ]
1518          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
1519          #Hlookup
1520          lapply (refl ? var_alloctype)
1521          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
1522          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
1523          [ (* stack alloc*)
1524            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1525            * #var_alloctype' #var_type' * #Hlookup_vartype'           
1526            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1527            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1528            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
1529            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
1530            @conj try @refl %4 whd in match (pointer_translation ??);
1531            >Hembed @refl
1532          | (* local alloc *)
1533            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1534            * #var_alloctype' #var_type' * #Hlookup_vartype'
1535            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1536            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1537            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
1538(*| 4: #e #ty*)
1539| 4:
1540  * #ed #ety cases ety
1541  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1542  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
1543  whd in match (typeof ?);
1544  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
1545  cases (bind_inversion ????? Htranslate) -Htranslate   
1546  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1547  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1548  * #cl_val #trace0 * #Hexec_expr #Hcl_val
1549  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
1550  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1551  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
1552  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
1553    [ 1,5,9,13: #Heq destruct (Heq)
1554    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
1555    | 3,7,11,15: #Heq destruct (Heq)
1556    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
1557  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
1558  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
1559  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
1560  %{cm_val} @conj try @refl try assumption
1561| 5:
1562  #ty cases ty
1563  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1564  | #structname #fieldspec | #unionname #fieldspec | #id ]
1565  #ed #ty' #Hind
1566  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
1567  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1568  cases (bind_inversion ????? Htranslate) -Htranslate
1569  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1570  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1571  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
1572  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1573  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1574  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
1575  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
1576  %{cm_val} @conj try @refl assumption
1577| 6:
1578  #ty *
1579  [ cases ty
1580    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1581    | #structname #fieldspec | #unionname #fieldspec | #id ]
1582    #e #Hind
1583    whd in match (typeof ?);
1584    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
1585    #Htranslate
1586    [ 3,4,5,8: destruct (Htranslate)
1587    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1588         cases sz normalize nodelta
1589         #e' #Hexpr_vars #Htranslate
1590         [ 1, 2: destruct (Htranslate) ] ]
1591    #cl_val #trace #Hyp_present #Hexec_expr
1592    cases (bind_inversion ????? Htranslate) -Htranslate
1593    #cmop * #Htranslate_unop #Hexec_arg
1594    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1595    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1596    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1597    * #cl_arg #cl_trace * #Hexec_cl
1598    whd in ⊢ ((???%) → ?); #Hexec_unop
1599    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1600    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1601    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1602    #Hsem_cl whd in match (eval_expr ???????);
1603    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1604    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1605    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
1606    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
1607    whd in match (typ_of_type Tvoid);
1608    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
1609    #H >H @refl
1610  | *:
1611    cases ty
1612    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
1613    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
1614    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
1615    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
1616    whd in Htranslate:(??%?);
1617    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
1618    cases (bind_inversion ????? Htranslate) -Htranslate
1619    #cmop * #Htranslate_unop #Hexec_arg
1620    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1621    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1622    cases (bind_inversion ????? Hexec) -Hexec
1623    * #cl_arg #cl_trace * #Hexec_cl
1624    whd in ⊢ ((???%) → ?); #Hexec_unop
1625    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1626    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1627    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1628    #Hcl_unop whd in match (eval_expr ???????);
1629    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1630    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1631    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
1632    * #op_res * #Hcl_sem #Hvalue_eq
1633    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
1634       %{op_res} @conj try @refl assumption
1635    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
1636       %{op_res} @conj try @refl assumption
1637    ]
1638  ]
1639| 8: #ty #ty' * #ed #ety
1640  cases ety
1641  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
1642  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
1643  whd in match (typeof ?); whd in match (typ_of_type ?);
1644  #Hind whd in match (typeof ?);
1645  #cm_expr #Hexpr_vars #Htranslate
1646  cases (bind_inversion ????? Htranslate) -Htranslate
1647  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
1648  cases (bind_inversion ????? Htranslate) -Htranslate
1649  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
1650  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
1651  cases (bind_inversion ????? Htranslate) -Htranslate
1652  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
1653  #Heq destruct (Heq)
1654  #cl_val #trace #Hyp_present #Hexec_cm
1655  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1656  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
1657  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
1658  #cast_val * #Hexec_cast
1659  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1660  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
1661  #Htype_eq
1662  lapply Hexec_cast -Hexec_cast
1663(*  lapply Htyp_should_eq -Htyp_should_eq *)
1664  lapply Htranslate_cast -Htranslate_cast
1665  lapply Hexpr_vars_cast -Hexpr_vars_cast
1666  lapply cm_cast -cm_cast
1667  lapply Hyp_present -Hyp_present
1668  lapply Hexpr_vars -Hexpr_vars
1669  lapply cm_expr -cm_expr
1670  <Htype_eq -Htype_eq
1671  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
1672  whd in match (typeof ?); normalize nodelta
1673  cases ty'
1674  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
1675  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
1676  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
1677  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
1678  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
1679  whd in Htranslate_cast:(??%%);
1680  whd in Hexpr_vars;
1681  destruct (Htranslate_cast)
1682  [ 1,2,3,4,7:
1683    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1684    * #cm_val' * #Heval_castee
1685    lapply Hexec_cm -Hexec_cm
1686    whd in Hexec_cast:(??%%);
1687    cases cm_val in Hexec_cast; normalize nodelta
1688    [ | #vsz #vi | | #vp
1689    | | #vsz #vi | | #vp
1690    | | #vsz #vi | | #vp
1691    | | #vsz #vi | | #vp
1692    | | #vsz #vi | | #vp ]
1693    [ 2,6,10,14,18:
1694    | *: #Habsurd destruct (Habsurd) ]
1695    #Hexec_cast #Hexec_cm #Hvalue_eq
1696    [ 1,2,3:
1697      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
1698      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
1699    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
1700    [ 1,2,4,5:
1701      cases (bind_inversion ????? Hexec_cast)
1702      whd in match (typeof ?);
1703      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
1704      whd in match (eq_rect_r ??????);
1705      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
1706      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
1707      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
1708      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
1709      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1710      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
1711      >Heval_castee normalize nodelta whd in match (eval_unop ????);
1712      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
1713      >Heq_vi >eq_bv_true normalize
1714      %{Vnull} @conj try @refl %3
1715    | 3: destruct (Hcl_val_eq)
1716          whd in match (eval_expr ???????);
1717          >Heval_castee normalize nodelta
1718          whd in match (eval_unop ????);
1719          cases esg normalize nodelta
1720          whd in match (opt_to_res ???); whd in match (m_bind ?????);
1721          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
1722          whd in match (eq_rect_r ??????);
1723          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
1724          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
1725             this reason. *)
1726          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
1727          cases esz normalize nodelta
1728          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
1729          whd in match (sign_ext ??); whd in match (zero_ext ??);
1730          %2
1731    ]
1732 | *:
1733    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1734    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
1735    %{cm_val'} @conj try @refl
1736    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
1737    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
1738    cases cm_val
1739    [ | #vsz #vi | | #vp
1740    | | #vsz #vi | | #vp
1741    | | #vsz #vi | | #vp
1742    | | #vsz #vi | | #vp ]
1743    #Hexec_cm #Hvalue_eq #Hexec_cast
1744    whd in Hexec_cast:(??%%);
1745    [ 1,5,9,13: destruct (Hexec_cast) ]
1746    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
1747    lapply Hexec_cast -Hexec_cast
1748    normalize cases (eq_v ?????) normalize
1749    #Habsurd destruct (Habsurd)
1750 ]
1751| 9: (* Econdition *) 
1752  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
1753  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
1754  #Hexec_cm
1755  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1756  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
1757  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1758  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
1759  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1760  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
1761  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1762  cases (bind_inversion ????? Htranslate) -Htranslate
1763  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1764  cases (bind_inversion ????? Htranslate) -Htranslate
1765  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
1766  cases (bind_inversion ????? Htranslate) -Htranslate
1767  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
1768  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
1769  *  #Htypeof_e2_eq_ty
1770  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1771  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
1772  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
1773  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1774  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
1775  cases (bind_inversion ????? Htranslate) -Htranslate
1776  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
1777  cases (bind_inversion ????? Htranslate) -Htranslate 
1778  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
1779  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
1780  * #Htypeof_e3_eq_ty
1781  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
1782  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
1783  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
1784  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1785  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
1786  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
1787  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
1788  lapply Hexec_bool_of_val -Hexec_bool_of_val
1789  cases (typeof e1) normalize nodelta
1790  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
1791  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
1792  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
1793  whd in Heq:(???%); destruct (Heq)
1794  whd in match (eval_expr ???????);
1795  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
1796  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
1797  >Heval_e1 normalize nodelta
1798  lapply Hcm_ifthenelse -Hcm_ifthenelse
1799  lapply Hexec_cond -Hexec_cond 
1800  lapply Hexec_bool_of_val -Hexec_bool_of_val
1801  lapply Hvalue_eq1 -Hvalue_eq1
1802  cases cm_cond_val
1803  [ | #vsz #vi | | #vp
1804  | | #vsz #vi | | #vp
1805  | | #vsz #vi | | #vp
1806  | | #vsz #vi | | #vp ]
1807  whd in ⊢ (? → (??%%) → ?);
1808  [ 6:
1809  | *: #_ #Habsurd destruct (Habsurd) ]
1810  #Hvalue_eq1 #Hsz_check
1811  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1812  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1813  #Heq destruct (Heq)
1814  #Hexec_expr_e1
1815  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
1816    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
1817    with
1818    [ true ⇒ λHeq. ?
1819    | false ⇒ λHeq. ?
1820    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
1821  normalize nodelta
1822  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
1823  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
1824  >Heq normalize nodelta
1825  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
1826    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
1827    normalize %{cm_val3} @conj try @refl assumption
1828  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
1829    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
1830    normalize %{cm_val2} @conj try @refl assumption ]
1831| 10: (* andbool *)
1832  #ty cases ty
1833  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1834  | #structname #fieldspec | #unionname #fieldspec | #id ]
1835  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
1836  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
1837  (* decompose first slice of clight execution *)
1838  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1839  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
1840  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1841  #b * #Hexec_bool_of_val #Hexec_expr
1842  (* decompose translation to Cminor *)
1843  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
1844  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1845  cases (bind_inversion ????? Htranslate) -Htranslate
1846  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
1847  [ 2: | *: #Heq destruct (Heq) ]
1848  (* discriminate I16 and I8 cases *)
1849(*  lapply Hyp_present -Hyp_present
1850  lapply Hexpr_vars -Hexpr_vars
1851  lapply cm_expr -cm_expr cases sz
1852  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
1853  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
1854  (* go on with decomposition *)
1855  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
1856  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
1857  (* cleanup the type coercion *)
1858  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
1859  * #Htypeof_e2_eq_ty
1860  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1861  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
1862  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
1863  lapply Hexpr_vars_e2 -Hexpr_vars_e2
1864  lapply cm_expr_e2 -cm_expr_e2
1865  lapply Hexec_expr -Hexec_expr
1866  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
1867  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
1868  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
1869  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
1870   * to proceed in decomposing translation. *)
1871  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
1872  lapply Hexpr_vars_e1 -Hexpr_vars_e1
1873  lapply cm_expr_e1 -cm_expr_e1
1874  lapply Hexec_bool_of_val -Hexec_bool_of_val
1875  cases (typeof e1)
1876  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1877  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1878  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
1879  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1880  (* translation decomposition terminated. Reduce goal *)
1881  whd in match (eval_expr ???????);
1882  (* We need Hind1.  *)
1883  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
1884  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
1885  normalize nodelta
1886  (* peform case analysis to further reduce the goal. *)
1887  lapply Hvalue_eq -Hvalue_eq
1888  lapply Hexec_bool_of_val -Hexec_bool_of_val
1889  whd in match (proj2 ???);
1890  cases cl_val_e1
1891  [ | #vsz #vi | | #vp
1892  | | #vsz #vi | | #vp
1893  | | #vsz #vi | | #vp
1894  | | #vsz #vi | | #vp ]
1895  whd in ⊢ ((??%%) → ?);
1896  [ 6:
1897  | *: #Heq destruct (Heq) ]
1898  #Hsz_check #Hvalue_eq
1899  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1900  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1901  (* preparing case analysis on b *)
1902  lapply Hexec_expr -Hexec_expr
1903  cases b normalize nodelta
1904  [ 2: (* early exit *)
1905       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
1906       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
1907       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
1908       <e0 whd in match (m_bind ?????);
1909       @cthulhu
1910       (* Pb: incompatible semantics for cl and cm.
1911        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
1912          first operand is false (for andbool)
1913          . solution 1 : change semantics to return actual value instead of Vfalse
1914          . solution 2 : change toCminor to introduce another test in the program,
1915            returning Vfalse in case of failure instead of actual value
1916        *) ]
1917  #Hexec_expr #Heq_outcome
1918  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1919  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
1920  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1921  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
1922  #Heq destruct (Heq)
1923  >(value_eq_int_inversion … Hvalue_eq)
1924  whd in match (eval_bool_of_val ?);
1925  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
1926  normalize nodelta
1927  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
1928  >Heval_expr normalize nodelta
1929  %{cm_val_e2} @conj try @refl 
1930  whd in Hexec_bool_outcome:(??%%);
1931  normalize nodelta in Hexec_bool_outcome:(??%%);
1932  lapply Hvalue_eq2 -Hvalue_eq2
1933  -Heval_expr
1934  lapply Hexec_bool_outcome -Hexec_bool_outcome
1935  cases cl_val_e2
1936  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
1937  #Heq destruct (Heq)
1938  cases (intsize_eq_elim_inversion ??????? Heq)
1939  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1940  cases outcome_bool normalize nodelta
1941  (* Problem. cf prev case. *)
1942  @cthulhu
1943| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
1944| 12: (* sizeof *)
1945  #ty cases ty
1946  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1947  | #structname #fieldspec | #unionname #fieldspec | #id ]
1948  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1949  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
1950  normalize in match (typ_of_type ?);
1951  whd in Htranslate:(??%?); destruct (Htranslate)
1952  whd in match (eval_expr ???????);
1953  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
1954| 13:
1955  #ty #ed #ty' cases ty'
1956  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1957  | #structname #fieldspec | #unionname #fieldspec | #id ]
1958  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
1959  #Hexec_lvalue
1960  whd in Hexec_lvalue:(??%?); destruct
1961  [ whd in Htranslate_addr:(??%?);
1962    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1963    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
1964    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1965    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
1966    #Heq destruct (Heq)
1967    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
1968  ]
1969  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1970  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
1971  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
1972       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
1973       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
1974       #cm_val_field * #Heval_cm #Hvalue_eq
1975       whd in match (eval_expr ???????);
1976       >Heval_cm normalize nodelta
1977       whd in match (eval_expr ???????); whd in match (m_bind ?????);
1978       whd in match (eval_binop ???????); normalize nodelta
1979       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
1980       normalize nodelta #Hptr_translate
1981       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
1982       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
1983       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
1984       cases (E cl_blo) in Hptr_translate; normalize nodelta
1985       [ #H destruct (H) ]
1986       * #BL #OFF normalize nodelta #Heq destruct (Heq)
1987       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
1988       #H destruct (H)
1989       (* again, mismatch in the size of the integers *)
1990       @cthulhu
1991  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
1992       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
1993       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
1994       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
1995       #Hpointer_translation
1996       %{cm_val} @conj try assumption
1997       destruct @refl
1998   ]
1999| 14: (* cost label *)
2000  #ty (* cases ty
2001  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2002  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
2003  #l * #ed #ety
2004  whd in match (typeof ?); whd in match (typeof ?);
2005  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2006  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2007  #Hexpr_vars * #Htranslate_ind #Htranslate
2008  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2009  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2010  whd in match (typeof ?) in Htyp_should_eq:(??%?);
2011  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
2012  #Htyp_eq
2013  lapply Htranslate_ind -Htranslate_ind
2014  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2015  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2016  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2017  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
2018  <Htyp_eq
2019  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
2020  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2021  whd in match (eval_expr ???????);
2022  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2023  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2024  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2025  #cm_val' * #Heval_expr' #Hvalue_eq
2026  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
2027  >cons_to_append >(nil_append … cm_trace) @refl
2028| 15: *
2029  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
2030  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
2031  #ty normalize in ⊢ (% → ?);
2032  [ 2,3,12: @False_ind
2033  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2034           normalize #Habsurd destruct (Habsurd) ]
2035] qed.
2036
2037
2038axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
2039
2040(* Conjectured simulation results
2041
2042   We split these based on the start state:
2043   
2044   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
2045      normal steps in Cminor;
2046   2. call and return steps are simulated by a call/return step plus [m] normal
2047      steps (to copy stack allocated parameters / results); and
2048   3. lone cost label steps are simulates by a lone cost label step
2049   
2050   These should allow us to maintain enough structure to identify the Cminor
2051   subtrace corresponding to a measurable Clight subtrace.
2052 *)
2053
2054definition clight_normal : Clight_state → bool ≝
2055λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2056
2057definition cminor_normal : Cminor_state → bool ≝
2058λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2059
2060axiom clight_cminor_normal :
2061  ∀INV:clight_cminor_inv.
2062  ∀s1,s1',s2,tr.
2063  clight_cminor_rel INV s1 s1' →
2064  clight_normal s1 →
2065  ¬ Clight_labelled s1 →
2066  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2067  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2068    tr = tr' ∧
2069    clight_cminor_rel INV s2 s2'
2070  ).
2071
2072axiom clight_cminor_call_return :
2073  ∀INV:clight_cminor_inv.
2074  ∀s1,s1',s2,tr.
2075  clight_cminor_rel INV s1 s1' →
2076  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2077  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2078  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2079    tr = tr' ∧
2080    clight_cminor_rel INV s2 s2'
2081  ).
2082
2083axiom clight_cminor_cost :
2084  ∀INV:clight_cminor_inv.
2085  ∀s1,s1',s2,tr.
2086  clight_cminor_rel INV s1 s1' →
2087  Clight_labelled s1 →
2088  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2089  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2090    tr = tr' ∧
2091    clight_cminor_rel INV s2 s2'
2092  ).
2093
Note: See TracBrowser for help on using the repository browser.