source: src/Clight/toCminorCorrectness.ma @ 2578

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

Progress on CL to CM, fixed some stuff in memory injections.

File size: 114.7 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
361lemma lookup_exec_alloc :
362  ∀source_variables, initial_env, env, var_id, clb, m, m'.
363  lookup ?? env var_id = Some ? clb →
364  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
365  lookup ?? initial_env var_id = Some ? clb ∨
366  Exists ? (λx. \fst x = var_id) source_variables.
367#source_variables
368elim source_variables
369[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
370     destruct (Hexec_alloc) %1 @Hlookup
371| 2: * #id #ty #tail #Hind
372     #init_env #env #var #clb #m #m' #Hlookup     
373     whd in ⊢ (??%? → ?);
374     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
375     #Hexec_alloc
376     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
377     [ 1: destruct (Heq) %2 %1 @refl ]
378     cases (Hind … Hlookup Hexec_alloc)
379     [ @cthulhu (* standard reasoning on positive_maps. check lib. *)
380     | #Hexists %2 %2 @Hexists ]
381] qed.
382
383lemma characterise_vars_lookup_local :
384  ∀globals,f,vartypes,stacksize,id,clb,env.
385   characterise_vars globals f = 〈vartypes, stacksize〉 →
386   lookup ?? env id = Some ? clb →
387   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
388   ∃t. local_id vartypes id t.
389#globals #f #vartypes #stacksize #id #clb #env
390#Hchar #Hlookup * #m * #m' #Hexec
391cases (lookup_exec_alloc … Hlookup Hexec)
392[ normalize in ⊢ (% → ?); #Heq destruct
393| @(characterise_vars_localid … Hchar) ]
394qed.
395
396
397lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
398  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
399  lookup ?? env' var_id = None ? →
400  lookup ?? env var_id = None ? ∧
401  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
402#vars elim vars
403[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
404  #H @conj try @H % //
405| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
406  whd in ⊢ ((??%?) → ? → ?);
407  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
408  normalize nodelta #Hexec #Hlookup
409  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
410  cases env #env cases id' #id' cases var #var normalize
411  @(eqb_elim … id' var)
412  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
413       #Heq <Heq @conj try @Hlookup' % *
414       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
415       | cases Hexists' #H @H ]
416  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
417       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
418       >H1 in Hlookup'; #Heq destruct
419  ]
420] qed.
421
422lemma variable_not_in_env_but_in_vartypes_is_global :
423  ∀env,env',f,vars,stacksize,globals,var_id.
424  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
425  characterise_vars globals f =〈vars,stacksize〉 →
426  lookup ?? env' var_id = None ? →       
427  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
428  ∃r.allocty = Global r.
429#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
430#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
431lapply (characterise_vars_src … Hcharacterise var_id ?)
432[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
433 #Hlookup >Hlookup #_ #Habsurd destruct ]
434*
435[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
436     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
437* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
438@(match allocty
439  return λx. allocty = x → ?
440  with
441  [ Global r ⇒ λ_. ?
442  | Stack st' ⇒ λHalloc. ?
443  | Local ⇒ λHalloc. ?
444  ] (refl ? allocty))
445[ @False_ind ] normalize nodelta
446#Heq_typ
447(* Halloc is in contradiction with Hlookup_fail *)
448lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
449* #Hlookup' #Hnot_exists
450lapply (characterise_vars_all … Hcharacterise var_id t ?)
451[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
452#Hexists @False_ind
453cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
454[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
455       * #id' #ty' #tl #Hind *
456       [ 1,3: * #Heq #_ %1 @Heq
457       | *: #H %2 @Hind @H ] ]
458#H cases Hnot_exists #H' @H' @H
459qed.
460
461
462lemma translate_notbool_to_cminor :
463  ∀t,sg,arg.
464  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
465  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
466        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
467*
468[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
469| #structname #fieldspec | #unionname #fieldspec | #id ]
470normalize in match (typ_of_type ?);
471#sg #arg #cmop
472whd in ⊢ (??%% → ?); #Heq destruct (Heq)
473cases arg
474[ | #vsz #vi | | #vp
475| | #vsz #vi | | #vp
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#res
483whd in ⊢ ((??%?) → ?);
484#Heq
485[ 6,11,12: | *: destruct (Heq) ]
486[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
487| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
488     #H normalize nodelta #Heq destruct
489     whd in match (eval_unop ????);
490     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
491] qed.
492
493lemma translate_notint_to_cminor :
494  ∀t,t',arg.
495  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
496  ∀res. sem_unary_operation Onotint arg t = Some ? res →
497        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
498#ty *
499[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
500#sz #sg #arg #cmop
501whd in match (translate_unop ???);
502@(match typ_eq (ASTint sz sg) (typ_of_type ty)
503  with
504  [ inl H ⇒ ?
505  | inr H ⇒ ? ])
506normalize nodelta
507[ 2: #Heq destruct ]
508lapply H -H
509lapply cmop -cmop
510cases ty
511[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
512| #structname #fieldspec | #unionname #fieldspec | #id ]
513normalize nodelta
514#cmop normalize in match (typ_of_type ?); #H destruct
515#H' normalize in H';
516destruct (H')
517#res
518whd in match (sem_unary_operation ???);
519cases arg
520[ | #vsz #vi | | #vp
521| | #vsz #vi | | #vp
522| | #vsz #vi | | #vp
523| | #vsz #vi | | #vp ]
524whd in match (sem_notint ?);
525#H destruct (H) @refl
526qed.
527
528
529lemma translate_negint_to_cminor :
530  ∀t,t',arg.
531  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
532  ∀res. sem_unary_operation Oneg arg t = Some ? res →
533        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
534#ty *
535[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
536#sz #sg #arg #cmop
537whd in match (translate_unop ???);
538@(match typ_eq (ASTint sz sg) (typ_of_type ty)
539  with
540  [ inl H ⇒ ?
541  | inr H ⇒ ? ])
542normalize nodelta
543[ 2: #Heq destruct ]
544lapply H -H
545lapply cmop -cmop
546cases ty
547[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
548| #structname #fieldspec | #unionname #fieldspec | #id ]
549normalize nodelta
550#cmop normalize in match (typ_of_type ?); #H destruct
551#H' normalize in H';
552destruct (H')
553#res
554whd in match (sem_unary_operation ???);
555cases arg
556[ | #vsz #vi | | #vp
557| | #vsz #vi | | #vp
558| | #vsz #vi | | #vp
559| | #vsz #vi | | #vp ]
560whd in match (sem_neg ??);
561#H destruct (H)
562whd in match (eval_unop ????);
563cases (eq_intsize sz' vsz) in H; normalize nodelta
564#H destruct @refl
565qed.
566
567
568lemma translate_unop :
569  ∀ty,sg,op,cmop.
570  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
571  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
572            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
573#ty #sg * #cmop #Htranslate #arg
574[ @translate_notbool_to_cminor assumption
575| @translate_notint_to_cminor assumption
576| @translate_negint_to_cminor assumption ]
577qed.
578
579lemma classify_add_inversion :
580  ∀ty1,ty2.
581    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
582    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
583    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
584    (classify_add ty1 ty2 = add_default ty1 ty2).
585#ty1 #ty2
586cases (classify_add ty1 ty2)
587[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
588| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
589| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
590| #tya #tyb %2 @refl ]
591qed.
592
593(*
594lemma classify_cmp_inversion :
595  ∀ty1,ty2.
596    if_type_eq ty1 ty2 (λty1, ty2. classify_cmp_cases ty1 ty2)
597    ((∃sz,sg. ty1 = Tint sz sg ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_ii sz sg) ∨
598     (∃ty'. ty1 = Tpointer ty' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (None ?) ty') ∨
599     (∃ty',n'. ty1 = Tarray ty' n' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (Some ? n') ty') ∨         
600    (classify_cmp ty1 ty2 = cmp_default …)
601*)   
602
603lemma classify_aop_inversion :
604  ∀ty1,ty2.
605    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
606    classify_aop ty1 ty2 = aop_default ty1 ty2.
607#ty1 #ty2
608cases (classify_aop ty1 ty2)
609[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
610| #ty #ty' %2 @refl ]
611qed.
612
613lemma sem_add_ip_inversion :
614  ∀sz,sg,ty',optlen.
615  ∀v1,v2,res.
616  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
617  ∃sz',i. v1 = Vint sz' i ∧
618      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
619       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
620#tsz #tsg #ty' * [ | #n ]
621*
622[ | #sz' #i' | | #p'
623| | #sz' #i' | | #p' ]
624#v2 #res
625whd in ⊢ ((??%?) → ?);
626#H destruct
627cases v2 in H;
628[ | #sz2' #i2' | | #p2'
629| | #sz2' #i2' | | #p2' ] normalize nodelta
630#H destruct
631[ 1,3:
632  lapply H -H
633  @(eq_bv_elim … i' (zero ?)) normalize nodelta
634  #Hi #Heq destruct (Heq)
635  %{sz'} %{(zero ?)} @conj destruct try @refl
636  %2 @conj try @conj try @refl
637| *: %{sz'} %{i'} @conj try @refl
638  %1 %{p2'} @conj try @refl
639] qed.
640
641(* symmetric of the upper one *)
642lemma sem_add_pi_inversion :
643  ∀sz,sg,ty',optlen.
644  ∀v1,v2,res.
645  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
646  ∃sz',i. v2 = Vint sz' i ∧
647      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
648       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
649#tsz #tsg #ty' * [ | #n ]
650*
651[ | #sz' #i' | | #p'
652| | #sz' #i' | | #p' ]
653#v2 #res
654whd in ⊢ ((??%?) → ?);
655#H destruct
656cases v2 in H; normalize nodelta
657[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
658#H destruct
659[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
660  %{p'} @conj try @refl
661| *: lapply H -H
662  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
663  #Hi #Heq destruct (Heq)
664  %{sz2'} %{(zero ?)} @conj destruct try @refl
665  %2 @conj try @conj try @refl
666] qed.
667
668(* Know that addition on integers gives an integer. Notice that there is no correlation
669   between the size in the types and the size of the integer values. *)
670lemma sem_add_ii_inversion :
671  ∀sz,sg.
672  ∀v1,v2,res.
673  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
674  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
675              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
676#sz #sg
677*
678[ | #sz' #i' | | #p' ]
679#v2 #res
680whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
681cases sz cases sg normalize nodelta
682#H destruct
683cases v2 in H; normalize nodelta
684#H1 destruct
685#H2 destruct #Heq %{sz'} lapply Heq -Heq
686cases sz' in i'; #i' 
687whd in match (intsize_eq_elim ???????);
688cases H1 in H2; #j' normalize nodelta
689#Heq destruct (Heq)
690%{i'} %{j'} @conj try @conj try @conj try @refl
691qed.
692
693lemma sem_mul_inversion :
694  ∀sz,sg.
695  ∀v1,v2,res.
696  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
697  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
698              res = Vint sz' (short_multiplication ? i1 i2).
699#sz #sg *
700[ | #sz' #i' | | #p' ]
701#v2 #res
702whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
703cases sz cases sg normalize nodelta
704#H destruct
705cases v2 in H; normalize nodelta
706#H1 destruct
707#H2 destruct #Heq %{sz'} lapply Heq -Heq
708cases sz' in i'; #i' 
709whd in match (intsize_eq_elim ???????);
710cases H1 in H2; #j' normalize nodelta
711#Heq destruct (Heq)
712%{i'} %{j'} @conj try @conj try @conj try @refl
713qed.
714
715
716lemma sem_div_inversion_s :
717  ∀sz.
718  ∀v1,v2,res.
719  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
720  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
721              match division_s ? i1 i2 with
722              [ Some q ⇒  res =  (Vint sz' q)
723              | None ⇒ False ].
724#sz *
725[ | #sz' #i' | | #p' ]
726#v2 #res
727whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
728>type_eq_dec_true normalize nodelta
729#H destruct
730cases v2 in H; normalize nodelta
731[ | #sz2' #i2' | | #p2' ]
732#Heq destruct
733%{sz'}
734lapply Heq -Heq
735cases sz' in i'; #i' 
736whd in match (intsize_eq_elim ???????);
737cases sz2' in i2'; #i2' normalize nodelta
738whd in match (option_map ????); #Hdiv destruct
739%{i'} %{i2'} @conj try @conj try @conj try @refl
740cases (division_s ???) in Hdiv;
741[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
742qed.
743
744lemma sem_div_inversion_u :
745  ∀sz.
746  ∀v1,v2,res.
747  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
748  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
749              match division_u ? i1 i2 with
750              [ Some q ⇒  res =  (Vint sz' q)
751              | None ⇒ False ].
752#sz *
753[ | #sz' #i' | | #p' ]
754#v2 #res
755whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
756>type_eq_dec_true normalize nodelta
757#H destruct
758cases v2 in H; normalize nodelta
759[ | #sz2' #i2' | | #p2' ]
760#Heq destruct
761%{sz'}
762lapply Heq -Heq
763cases sz' in i'; #i' 
764whd in match (intsize_eq_elim ???????);
765cases sz2' in i2'; #i2' normalize nodelta
766whd in match (option_map ????); #Hdiv destruct
767%{i'} %{i2'} @conj try @conj try @conj try @refl
768cases (division_u ???) in Hdiv;
769[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
770qed.
771
772lemma sem_mod_inversion_s :
773  ∀sz.
774  ∀v1,v2,res.
775  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
776  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
777              match modulus_s ? i1 i2 with
778              [ Some q ⇒  res =  (Vint sz' q)
779              | None ⇒ False ].
780#sz *
781[ | #sz' #i' | | #p' ]
782#v2 #res
783whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
784>type_eq_dec_true normalize nodelta
785#H destruct
786cases v2 in H; normalize nodelta
787[ | #sz2' #i2' | | #p2' ]
788#Heq destruct
789%{sz'}
790lapply Heq -Heq
791cases sz' in i'; #i' 
792whd in match (intsize_eq_elim ???????);
793cases sz2' in i2'; #i2' normalize nodelta
794whd in match (option_map ????); #Hdiv destruct
795%{i'} %{i2'} @conj try @conj try @conj try @refl
796cases (modulus_s ???) in Hdiv;
797[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
798qed.
799
800lemma sem_mod_inversion_u :
801  ∀sz.
802  ∀v1,v2,res.
803  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
804  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
805              match modulus_u ? i1 i2 with
806              [ Some q ⇒  res =  (Vint sz' q)
807              | None ⇒ False ].
808#sz *
809[ | #sz' #i' | | #p' ]
810#v2 #res
811whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
812>type_eq_dec_true normalize nodelta
813#H destruct
814cases v2 in H; normalize nodelta
815[ | #sz2' #i2' | | #p2' ]
816#Heq destruct
817%{sz'}
818lapply Heq -Heq
819cases sz' in i'; #i' 
820whd in match (intsize_eq_elim ???????);
821cases sz2' in i2'; #i2' normalize nodelta
822whd in match (option_map ????); #Hdiv destruct
823%{i'} %{i2'} @conj try @conj try @conj try @refl
824cases (modulus_u ???) in Hdiv;
825[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
826qed.
827
828lemma sem_and_inversion :
829  ∀v1,v2,res.
830  sem_and v1 v2 = Some ? res →
831  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
832              res = Vint sz' (conjunction_bv ? i1 i2).
833*
834[ | #sz' #i' | | #p' ]
835#v2 #res
836whd in ⊢ ((??%?) → ?);
837#H destruct
838cases v2 in H; normalize nodelta
839[ | #sz2' #i2' | | #p2' ]
840#Heq destruct
841%{sz'}
842lapply Heq -Heq
843cases sz' in i'; #i' 
844whd in match (intsize_eq_elim ???????);
845cases sz2' in i2'; #i2' normalize nodelta
846#H destruct
847%{i'} %{i2'} @conj try @conj try @conj try @refl
848qed.
849
850lemma sem_or_inversion :
851  ∀v1,v2,res.
852  sem_or v1 v2 = Some ? res →
853  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
854              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
855*
856[ | #sz' #i' | | #p' ]
857#v2 #res
858whd in ⊢ ((??%?) → ?);
859#H destruct
860cases v2 in H; normalize nodelta
861[ | #sz2' #i2' | | #p2' ]
862#Heq destruct
863%{sz'}
864lapply Heq -Heq
865cases sz' in i'; #i' 
866whd in match (intsize_eq_elim ???????);
867cases sz2' in i2'; #i2' normalize nodelta
868#H destruct
869%{i'} %{i2'} @conj try @conj try @conj try @refl
870qed.
871
872lemma sem_xor_inversion :
873  ∀v1,v2,res.
874  sem_xor v1 v2 = Some ? res →
875  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
876              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
877*
878[ | #sz' #i' | | #p' ]
879#v2 #res
880whd in ⊢ ((??%?) → ?);
881#H destruct
882cases v2 in H; normalize nodelta
883[ | #sz2' #i2' | | #p2' ]
884#Heq destruct
885%{sz'}
886lapply Heq -Heq
887cases sz' in i'; #i' 
888whd in match (intsize_eq_elim ???????);
889cases sz2' in i2'; #i2' normalize nodelta
890#H destruct
891%{i'} %{i2'} @conj try @conj try @conj try @refl
892qed.
893
894lemma sem_shl_inversion :
895  ∀v1,v2,res.
896  sem_shl v1 v2 = Some ? res →
897  ∃sz1,sz2,i1,i2.
898              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
899              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
900                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
901              lt_u (bitsize_of_intsize sz2) i2
902                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
903*
904[ | #sz' #i' | | #p' ]
905#v2 #res
906whd in ⊢ ((??%?) → ?);
907#H destruct
908cases v2 in H; normalize nodelta
909[ | #sz2' #i2' | | #p2' ]
910#Heq destruct
911%{sz'} %{sz2'}
912lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
913%{i'} %{i2'}
914>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
915qed.
916
917lemma sem_shr_inversion :
918  ∀v1,v2,sz,sg,res.
919  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
920  ∃sz1,sz2,i1,i2.
921              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
922              lt_u (bitsize_of_intsize sz2) i2
923                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
924              match sg with
925              [ Signed ⇒
926                 res =
927                   (Vint sz1
928                    (shift_right bool (7+pred_size_intsize sz1*8)
929                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
930                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
931              | Unsigned ⇒
932                 res =
933                   (Vint sz1
934                    (shift_right bool (7+pred_size_intsize sz1*8)
935                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
936              ].
937*
938[ | #sz' #i' | | #p' ]
939#v2 #sz * #res
940whd in ⊢ ((??%?) → ?);
941whd in match (classify_aop ??);
942>type_eq_dec_true normalize nodelta
943#H destruct
944cases v2 in H; normalize nodelta
945[ | #sz2' #i2' | | #p2'
946| | #sz2' #i2' | | #p2' ]
947#Heq destruct
948%{sz'} %{sz2'}
949lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
950%{i'} %{i2'}
951>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
952qed.
953
954lemma complete_cmp_inversion :
955  ∀ty:type.
956  ∀e:expr (ASTint I8 Unsigned).
957  ∀r:expr (typ_of_type ty).
958   complete_cmp ty e = return r →
959   ∃sz,sg. ty = Tint sz sg ∧
960           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
961*
962[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
963| #structname #fieldspec | #unionname #fieldspec | #id ]
964#e whd in match (typ_of_type ?);
965#r whd in ⊢ ((??%%) → ?);
966#H destruct
967%{sz} %{sg} @conj try @refl @refl_jmeq
968qed.
969
970
971lemma sem_cmp_int_inversion :
972  ∀v1,v2,sz,sg,op,m,res.
973   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
974   ∃sz,i1,i2. v1 = Vint sz i1 ∧
975              v2 = Vint sz i2 ∧
976    match sg with
977    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
978    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
979    ].
980#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
981whd in ⊢ ((??%?) → ?);
982whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
983cases v1
984[ | #sz #i | | #p ] normalize nodelta
985#H destruct
986cases v2 in H;
987[ | #sz' #i' | | #p' ] normalize nodelta
988#H destruct lapply H -H
989cases sz in i; #i
990cases sz' in i'; #i' cases sg normalize nodelta
991whd in match (intsize_eq_elim ???????); #H destruct
992[ 1,2: %{I8}
993| 3,4: %{I16}
994| 5,6: %{I32} ] 
995%{i} %{i'} @conj try @conj try @refl
996qed.
997
998lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
999#ty' * // qed.
1000
1001lemma sem_cmp_ptr_inversion :
1002  ∀v1,v2,ty',n,op,m,res.
1003   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
1004   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
1005                 valid_pointer m p1 = true ∧
1006                 valid_pointer m p2 = true ∧
1007                 (if eq_block (pblock p1) (pblock p2)
1008                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
1009                  else sem_cmp_mismatch op) = Some ? res) ∨
1010   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
1011   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
1012   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
1013* [ | #sz #i | | #p ] normalize nodelta
1014#v2 #ty' #n #op
1015* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
1016whd in match (classify_cmp ??); cases n normalize nodelta
1017[ 2,4,6,8: #array_len ]
1018whd in match (ptr_type ty' ?);
1019whd in match (if_type_eq ?????);
1020>type_eq_dec_true normalize nodelta
1021#H destruct
1022cases v2 in H; normalize nodelta
1023[ | #sz' #i' | | #p'
1024| | #sz' #i' | | #p'
1025| | #sz' #i' | | #p'
1026| | #sz' #i' | | #p' ]
1027#H destruct
1028try /6 by or_introl, or_intror, ex_intro, conj/
1029[ 1: %1 %1 %2 %{p} @conj try @conj //
1030| 3: %1 %1 %2 %{p} @conj try @conj //
1031| *: %1 %1 %1 %{p} %{p'}
1032     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
1033     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
1034     try @conj try @conj try @conj try @conj try @conj try @refl try @H
1035     destruct
1036] qed.
1037
1038lemma pointer_translation_eq_block :
1039  ∀E,p1,p2,p1',p2'.
1040  pointer_translation p1 E = Some ? p1' →
1041  pointer_translation p2 E = Some ? p2' →
1042  eq_block (pblock p1) (pblock p2) = true →
1043  eq_block (pblock p1') (pblock p2') = true.
1044#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
1045#H1 #H2 #Heq_block
1046lapply (eq_block_to_refl … Heq_block) #H destruct (H)
1047lapply H1 lapply H2 -H1 -H2
1048whd in ⊢ ((??%?) → (??%?) → ?);
1049cases (E b2) normalize nodelta
1050[ #Habsurd destruct ]
1051* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
1052@eq_block_b_b
1053qed.
1054
1055(*
1056lemma pointer_translation_cmp_offset :
1057  ∀E,p1,p2,p1',p2',op.
1058  pblock p1 = pblock p2 →
1059  pointer_translation p1 E = Some ? p1' →
1060  pointer_translation p2 E = Some ? p2' →
1061  cmp_offset op (poff p1) (poff p2) = cmp_offset op (poff p1') (poff p2').
1062#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' #op #Heq destruct
1063whd in ⊢ ((??%?) → (??%?) → ?);
1064cases (E b2) normalize nodelta
1065[ #H destruct ]
1066* #bx #ox normalize nodelta
1067#Heq1 #Heq2 destruct cases op
1068[ @sym_eq @eq_offset_translation
1069| @sym_eq @neq_offset_translation
1070| @cthulhu (* !!!! TODO !!!! *)
1071| @cthulhu (* !!!! TODO !!!! *)
1072| @cthulhu (* !!!! TODO !!!! *)
1073| @cthulhu (* !!!! TODO !!!! *)
1074] qed. *)
1075
1076(* The two following lemmas are just noise. *)
1077
1078lemma expr_vars_fix_ptr_type :
1079  ∀ty',optlen.
1080  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
1081  ∀P.
1082   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
1083   expr_vars
1084    (typ_of_type
1085        match optlen 
1086        in option 
1087        return λ_:(option ℕ).type with 
1088        [None⇒Tpointer ty'
1089        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
1090#ty' * normalize
1091[ 2: #n ]
1092#e #P
1093@expr_vars_mp //
1094qed.
1095
1096lemma eval_expr_rewrite_aux :
1097  ∀genv.
1098  ∀optlen.
1099  ∀ty'.
1100  ∀e.
1101  ∀cm_env.
1102  ∀H.
1103  ∀sp.
1104  ∀m.
1105  ∀res.
1106  (eval_expr genv
1107             (typ_of_type
1108                 match optlen in option return λ_:(option ℕ).type with 
1109                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
1110             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 →
1111   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
1112#genv * [ 2: #n ] normalize nodelta
1113#ty' normalize in match (typ_of_type ?);
1114#e #cm_env whd in match (fix_ptr_type ???);
1115#H #sp #m #res #H @H
1116qed.
1117
1118
1119(* TODOs : there are some glitches between clight and cminor :
1120 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
1121      in the shortcut case, the cminor code returns directly the outcome of the
1122      evaluated expr, with a possibly different size.
1123   2) another glitch is for the integer/pointer additions: Clight always performs
1124      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
1125      the sign of i, producing either a sign extension or a zero extension.
1126   3) something similar to 1) happens for binary comparison operators. Clight generates
1127      systematically a 32 bit value for the outcome of the comparison and lives with it,
1128      but toCminor actually generates something 8 bit and casts it back to the context type.
1129   4) we need some proof that we don't blow the stack during the transformation. Otherwise,
1130      a problem appears when we prove semantics preservation for pointer < comparison
1131      (we might wrap up the rhs and end SNAFU).
1132 *)
1133 
1134lemma eval_expr_sim :
1135  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
1136  ∀cl_cm_inv  : clight_cminor_inv.
1137  (* current function (defines local environment) *)
1138  ∀f          : function.
1139  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
1140  ∀alloctype  : var_types.
1141  ∀stacksize  : ℕ.
1142  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
1143  (* environments *)
1144  ∀cl_env     : cl_env.
1145  ∀cm_env     : cm_env.
1146  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
1147  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
1148  (* CL and CM memories *)
1149  ∀cl_m       : mem.
1150  ∀cm_m       : mem.
1151  (* memory injection and matching *)
1152  ∀embed      : embedding.
1153  ∀injection  : memory_inj embed cl_m cm_m.
1154  ∀stackptr   : block.
1155  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
1156  (* clight expr to cminor expr *)
1157  (∀(e:expr).
1158   ∀(e':CMexpr (typ_of_type (typeof e))).
1159   ∀Hexpr_vars.
1160   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
1161   ∀cl_val,trace,Hyp_present.
1162   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
1163   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
1164            value_eq embed cl_val cm_val) ∧
1165   (* clight /lvalue/ to cminor /expr/ *)
1166  (∀ed,ty.
1167   ∀(e':CMexpr ASTptr).
1168   ∀Hexpr_vars.
1169   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
1170   ∀cl_blo,cl_off,trace,Hyp_present.
1171   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
1172   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
1173            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
1174#inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
1175@expr_lvalue_ind_combined
1176[ 7: (* binary ops *)
1177     #ty
1178     #op #e1 #e2
1179     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
1180     cases (bind_inversion ????? Htranslate) -Htranslate
1181     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
1182     cases (bind_inversion ????? Htranslate) -Htranslate
1183     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
1184     whd in ⊢ ((??%?) → ?);
1185     #Htranslate_binop
1186     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
1187     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1188     #cl_val #trace #Hyp_present #Hexec
1189     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
1190     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
1191     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
1192     lapply Hyp_present -Hyp_present
1193     lapply Htranslate_lhs -Htranslate_lhs
1194     lapply Htranslate_rhs -Htranslate_rhs
1195     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
1196     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
1197     lapply Hexec -Hexec
1198     lapply Htranslated_binop -Htranslated_binop
1199     lapply rhs -rhs lapply lhs -lhs
1200     (* end of dump *)
1201     cases op
1202     whd in ⊢ (? → ? → (??%?) → ?);
1203     [ 1: (* add *)
1204       lapply (classify_add_inversion (typeof e1) (typeof e2))
1205       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1206       (* trying to factorise as much stuff as possible ... *)
1207       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
1208       * [ 1: * ]
1209       [ 1: * #sz * #sg * *
1210       | 2: * #optlen * #ty' * #sz * #sg * *
1211       | 3: * #optlen * #sz * #sg * #ty' * * ]
1212       whd in match (typeof ?) in ⊢ (% → % → ?);
1213       #Htypeof_e1 #Htypeof_e2
1214       >Htypeof_e1 >Htypeof_e2
1215       #Hclassify
1216       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1217       normalize nodelta
1218       whd in match (typeof ?) in ⊢ (% → % → %);
1219       whd in match (typ_of_type (Tint ??));
1220       #lhs #rhs #Htyp_should_eq
1221       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1222       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
1223       -Htyp_should_eq
1224       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1225       <Heq_e' -Heq_e'
1226       #Hexec
1227       #Hexpr_vars_rhs #Hexpr_vars_lhs
1228       #Htranslate_rhs #Htranslate_lhs
1229       * [ #Hyp_present_lhs #Hyp_present_rhs
1230         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
1231         | #Hyp_present_rhs * #Hyp_present_lhs #Hyp_present_cst  ]
1232       whd in match (typeof ?);
1233       #Hind_rhs #Hind_lhs
1234       cases (bind_inversion ????? Hexec) -Hexec
1235       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1236       cases (bind_inversion ????? Hexec) -Hexec
1237       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1238       cases (bind_inversion ????? Hexec) -Hexec
1239       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1240       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1241       whd in match (typeof ?); whd in match (typeof ?);
1242       #Hsem_binary
1243       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1244       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
1245       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1246       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1247       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
1248       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1249       whd in match (eval_expr ???????);
1250       whd in match (proj1 ???);
1251       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
1252       [ 1,2: >Heval_lhs normalize nodelta
1253              whd in match (eval_expr ???????);
1254              whd in match (eval_expr ???????);
1255              >Heval_rhs normalize nodelta
1256              whd in match (m_bind ?????);
1257       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1258            whd in match (eval_expr ???????);
1259            whd in match (eval_expr ???????);
1260            >Heval_lhs normalize nodelta
1261       ]
1262       whd in match (proj1 ???); whd in match (proj2 ???);
1263       [ 2: (* standard int/int addition. *)
1264            whd in match (eval_binop ???????);
1265            whd in Hsem_binary:(??%?);
1266            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1267            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1268            cases (sem_add_ii_inversion … Hsem_binary_translated)
1269            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1270            #Hcm_lhs #Hcm_rhs #Hcm_val
1271            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1272            >intsize_eq_elim_true normalize nodelta
1273            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1274            @conj try @refl lapply Hsem_binary_translated
1275            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
1276            >inttyp_eq_elim_true' normalize nodelta
1277            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
1278       | *: (* pointer/int int/pointer addition *)
1279            whd in Hsem_binary:(??%?);
1280            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1281            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1282            [ 1: lapply (sem_add_pi_inversion … Hsem_binary_translated)
1283                 * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
1284                 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
1285                 | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
1286                 destruct
1287                 whd in match (eval_unop ????);
1288                 @(match sg
1289                   return λs. sg = s → ?
1290                   with
1291                   [ Unsigned ⇒ λHsg. ?
1292                   | Signed ⇒ λHsg. ?
1293                   ] (refl ??)) normalize nodelta
1294                   whd in match (eval_binop ???????);
1295                   whd in match (m_bind ?????);
1296                   [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1297                                   (short_multiplication (bitsize_of_intsize I16)
1298                                   (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1299                                   (repr I16 (sizeof ty')))))}
1300                   | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1301                                   (short_multiplication (bitsize_of_intsize I16)
1302                                   (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1303                                   (repr I16 (sizeof ty')))))} ]
1304                   [ 1,2: @conj whd in match (E0); whd in match (Eapp trace_rhs ?);
1305                          >(append_nil … trace_rhs) try @refl
1306                          @(value_eq_triangle_diagram … Hvalue_eq_res)
1307                          whd in match (shift_pointer_n ????);
1308                          whd in match (shift_offset_n ????);
1309                          >commutative_short_multiplication
1310                          whd in match (shift_pointer ???);
1311                          whd in match (shift_offset ???);
1312                          @cthulhu (* cf problem description at top of lemma. *)
1313                   | 3: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1314                        >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1315                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1316                        normalize >append_nil try @refl
1317                   | 4: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1318                        >(short_multiplication_zero 16 (repr I16 (sizeof ty')))
1319                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1320                        normalize >append_nil try @refl ]
1321            | 2: (* integer/pointer add: symmetric to the case above. *) @cthulhu ]
1322       ]
1323     | 2: (* subtraction cases: identical to add *) @cthulhu
1324     | 3: (* mul *)
1325       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1326       [ 2,4: #Hclassify >Hclassify normalize nodelta
1327            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1328       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1329       whd in match (typeof ?); #e'
1330       * #sz * #sg * *
1331       whd in match (typeof ?) in ⊢ (% → % → ?);
1332       #Htypeof_e1 #Htypeof_e2
1333       >Htypeof_e1 >Htypeof_e2
1334       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1335       #Hclassify
1336       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1337       normalize nodelta
1338       whd in match (typ_of_type (Tint ??));
1339       #lhs #rhs #Htyp_should_eq
1340       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1341       -Htyp_should_eq
1342       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1343       <Heq_e' -Heq_e'
1344       #Hexec
1345       #Hexpr_vars_rhs #Hexpr_vars_lhs
1346       #Htranslate_rhs #Htranslate_lhs
1347       * #Hyp_present_lhs #Hyp_present_rhs
1348       #Hind_rhs #Hind_lhs
1349       cases (bind_inversion ????? Hexec) -Hexec
1350       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1351       cases (bind_inversion ????? Hexec) -Hexec
1352       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1353       cases (bind_inversion ????? Hexec) -Hexec
1354       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1355       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1356       whd in match (typeof ?); whd in match (typeof ?);
1357       #Hsem_binary
1358       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1359       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1360       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1361       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1362       whd in match (eval_expr ???????);
1363       whd in match (proj1 ???);
1364       >Heval_lhs normalize nodelta
1365       >Heval_rhs normalize nodelta
1366       whd in match (m_bind ?????);
1367       whd in match (eval_binop ???????);
1368       whd in Hsem_binary:(??%?);
1369       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1370       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1371       cases (sem_mul_inversion … Hsem_binary)
1372       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1373       #Hcm_lhs #Hcm_rhs #Hcm_val
1374       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1375       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1376       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1377       >intsize_eq_elim_true normalize nodelta
1378       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1379       @conj try @refl
1380       whd in Hsem_binary:(??%?);     
1381       whd in match (classify_aop ??) in Hsem_binary:(??%?);
1382       >type_eq_dec_true in Hsem_binary; normalize nodelta
1383       >intsize_eq_elim_true #Heq destruct (Heq)
1384       %2
1385     | 4,5: (* div *)
1386       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1387       [ 2,4: #Hclassify >Hclassify normalize nodelta
1388            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1389       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1390       whd in match (typeof ?); #e'
1391       * #sz * * * *
1392       whd in match (typeof ?) in ⊢ (% → % → ?);
1393       #Htypeof_e1 #Htypeof_e2
1394       >Htypeof_e1 >Htypeof_e2
1395       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1396       #Hclassify
1397       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1398       normalize nodelta
1399       whd in match (typ_of_type (Tint ??));
1400       #lhs #rhs #Htyp_should_eq
1401       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1402       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1403       -Htyp_should_eq
1404       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1405       <Heq_e' -Heq_e'
1406       #Hexec
1407       #Hexpr_vars_rhs #Hexpr_vars_lhs
1408       #Htranslate_rhs #Htranslate_lhs
1409       * #Hyp_present_lhs #Hyp_present_rhs
1410       #Hind_rhs #Hind_lhs
1411       cases (bind_inversion ????? Hexec) -Hexec
1412       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1413       cases (bind_inversion ????? Hexec) -Hexec
1414       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1415       cases (bind_inversion ????? Hexec) -Hexec
1416       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1417       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1418       whd in match (typeof ?); whd in match (typeof ?);
1419       #Hsem_binary
1420       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1421       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1422       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1423       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1424       whd in match (eval_expr ???????);
1425       whd in match (proj1 ???);
1426       >Heval_lhs normalize nodelta
1427       >Heval_rhs normalize nodelta
1428       whd in match (m_bind ?????);
1429       whd in match (eval_binop ???????);
1430       whd in Hsem_binary:(??%?);
1431       [ 1,3: (* div*)
1432          lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1433          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1434          [ cases (sem_div_inversion_s … Hsem_binary)
1435          | cases (sem_div_inversion_u … Hsem_binary) ]
1436       | 2,4: (* mod *)
1437          lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1438          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1439          [ cases (sem_mod_inversion_s … Hsem_binary)
1440          | cases (sem_mod_inversion_u … Hsem_binary) ]
1441       ]
1442       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1443       #Hcm_lhs #Hcm_rhs #Hcm_val
1444       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1445       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1446       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1447       >intsize_eq_elim_true normalize nodelta
1448       [ cases (division_s ???) in Hcm_val;
1449       | cases (division_u ???) in Hcm_val;
1450       | cases (modulus_s ???) in Hcm_val;
1451       | cases (modulus_u ???) in Hcm_val; ]
1452       normalize nodelta
1453       [ 1,3,5,7: @False_ind ]
1454       #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
1455     | 6,7,8: (* and,or,xor *)
1456       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1457       [ 2,4,6: #Hclassify >Hclassify normalize nodelta
1458            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1459       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1460       whd in match (typeof ?); #e'
1461       * #sz * #sg * *
1462       whd in match (typeof ?) in ⊢ (% → % → ?);
1463       #Htypeof_e1 #Htypeof_e2
1464       >Htypeof_e1 >Htypeof_e2
1465       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1466       #Hclassify
1467       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1468       normalize nodelta
1469       whd in match (typ_of_type (Tint ??));
1470       #lhs #rhs #Htyp_should_eq
1471       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1472       -Htyp_should_eq
1473       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1474       <Heq_e' -Heq_e'
1475       #Hexec
1476       #Hexpr_vars_rhs #Hexpr_vars_lhs
1477       #Htranslate_rhs #Htranslate_lhs
1478       * #Hyp_present_lhs #Hyp_present_rhs
1479       #Hind_rhs #Hind_lhs
1480       cases (bind_inversion ????? Hexec) -Hexec
1481       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1482       cases (bind_inversion ????? Hexec) -Hexec
1483       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1484       cases (bind_inversion ????? Hexec) -Hexec
1485       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1486       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1487       whd in match (typeof ?); whd in match (typeof ?);
1488       #Hsem_binary
1489       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1490       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1491       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1492       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1493       whd in match (eval_expr ???????);
1494       whd in match (proj1 ???);
1495       >Heval_lhs normalize nodelta
1496       >Heval_rhs normalize nodelta
1497       whd in match (m_bind ?????);
1498       whd in match (eval_binop ???????);
1499       whd in Hsem_binary:(??%?);
1500       [ 1: (* and *)
1501          lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1502           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1503          cases (sem_and_inversion … Hsem_binary)
1504       | 2: (* or *)
1505          lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1506           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1507          cases (sem_or_inversion … Hsem_binary)
1508       | 3: (* xor *)
1509          lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1510           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1511          cases (sem_xor_inversion … Hsem_binary)
1512       ]
1513       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1514       #Hcm_lhs #Hcm_rhs #Hcm_val
1515       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1516       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1517       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1518       >intsize_eq_elim_true normalize nodelta
1519       [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
1520       | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1521       | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1522       ]
1523       @conj try @refl >Hcm_val %2
1524     | 9,10: (* shl, shr *)
1525       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1526       [ 2,4: #Hclassify >Hclassify normalize nodelta
1527            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1528       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1529       whd in match (typeof ?); #e'
1530       * #sz * * * *
1531       whd in match (typeof ?) in ⊢ (% → % → ?);
1532       #Htypeof_e1 #Htypeof_e2
1533       >Htypeof_e1 >Htypeof_e2
1534       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1535       #Hclassify
1536       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1537       normalize nodelta
1538       whd in match (typ_of_type (Tint ??));
1539       #lhs #rhs #Htyp_should_eq
1540       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1541       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1542       -Htyp_should_eq
1543       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1544       <Heq_e' -Heq_e'
1545       #Hexec
1546       #Hexpr_vars_rhs #Hexpr_vars_lhs
1547       #Htranslate_rhs #Htranslate_lhs
1548       * #Hyp_present_lhs #Hyp_present_rhs
1549       #Hind_rhs #Hind_lhs
1550       cases (bind_inversion ????? Hexec) -Hexec
1551       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1552       cases (bind_inversion ????? Hexec) -Hexec
1553       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1554       cases (bind_inversion ????? Hexec) -Hexec
1555       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1556       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1557       whd in match (typeof ?); whd in match (typeof ?);
1558       #Hsem_binary
1559       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1560       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1561       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1562       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1563       whd in match (eval_expr ???????);
1564       whd in match (proj1 ???);
1565       >Heval_lhs normalize nodelta
1566       >Heval_rhs normalize nodelta
1567       whd in match (m_bind ?????);
1568       whd in match (eval_binop ???????);
1569       whd in Hsem_binary:(??%?);
1570       [ 1,3: (* shl *)
1571          lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1572          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1573          cases (sem_shl_inversion … Hsem_binary)
1574          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1575          #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
1576          destruct (Hcl_lhs Hcl_rhs)
1577          >(value_eq_int_inversion … Hvalue_eq_lhs)
1578          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1579          >Hshift_ok normalize nodelta
1580          %{(Vint sz1
1581               (shift_left bool (bitsize_of_intsize sz1)
1582               (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
1583          @conj try @refl >Hcl_val %2
1584       | *: (* shr, translated to mod /!\ *)     
1585          lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1586          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1587          cases (sem_shr_inversion … Hsem_binary) normalize nodelta
1588          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1589          #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
1590          destruct (Hcl_lhs Hcl_rhs)
1591          >(value_eq_int_inversion … Hvalue_eq_lhs)
1592          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1593          >Hshift_ok normalize nodelta >Hcl_val
1594          /3 by ex_intro, conj, vint_eq/ ]
1595     | *: (* comparison operators *)
1596       lapply e' -e'
1597       cases e1 #ed1 #ety1
1598       cases e2 #ed2 #ety2
1599       whd in match (typeof ?) in ⊢ (% → % → % → %);
1600       #cm_expr whd in match (typeof ?);
1601       inversion (classify_cmp ety1 ety2)
1602       [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
1603            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1604            lapply (jmeq_to_eq ??? Hety1) #Hety2'
1605            destruct #Hclassify >Hclassify normalize nodelta
1606            #cmexpr1 #cmexpr2
1607            whd in ⊢ ((???%) → ?);
1608            #Heq destruct (Heq)
1609       | 1,4,7,10,13,16:
1610            #sz #sg #Hety1 #Hety2 #Hclassify
1611            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1612            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1613            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1614            whd in match (typeof ?) in ⊢ (% → % → % → %);
1615            whd in match (typ_of_type ?) in ⊢ (% → % → ?);
1616            cases sg #cmexpr1 #cmexpr2 normalize nodelta
1617            #Hcast_to_bool #Hexec_expr
1618            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1619            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1620            destruct (Htyis_int)
1621            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1622            destruct (Hcm_expr)
1623            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1624            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1625            cases (bind_inversion ????? Hexec) -Hexec
1626            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1627            cases (bind_inversion ????? Hexec) -Hexec
1628            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1629            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1630            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
1631            #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
1632            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
1633            destruct (Hcl_lhs) destruct (Hcl_rhs)
1634            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
1635            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1636            * #Hyp_present_lhs #Hyp_present_rhs
1637            #Hind_rhs #Hind_lhs
1638            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1639            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1640            lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1641            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1642            whd in match (eval_expr ???????);
1643            whd in match (eval_expr ???????);
1644            >Heval_lhs normalize nodelta
1645            >Heval_rhs normalize nodelta
1646            whd in match (m_bind ?????);
1647            whd in match (eval_binop ???????);
1648            >(value_eq_int_inversion … Hvalue_eq_lhs)
1649            >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1650            >intsize_eq_elim_true normalize nodelta
1651            destruct (Heq_bool)
1652            whd in match (eval_unop ????);
1653            whd in match (opt_to_res ???);
1654            whd in match (m_bind ?????);
1655            (* finished modulo glitch in integer widths *)
1656            @cthulhu
1657       | *:
1658            #n #ty' #Hety1 #Hety2 #Hclassify
1659            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1660            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1661            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1662            whd in match (typeof ?) in ⊢ (% → % → % → %);
1663            #cmexpr1 #cmexpr2
1664            #Hcast_to_bool #Hexec_expr
1665            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1666            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1667            destruct (Htyis_int)
1668            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1669            destruct (Hcm_expr)
1670            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1671            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1672            cases (bind_inversion ????? Hexec) -Hexec
1673            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1674            cases (bind_inversion ????? Hexec) -Hexec
1675            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1676            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1677            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
1678            #Hsem_cmp (* cut > *)
1679            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1680            * #Hyp_present_lhs #Hyp_present_rhs
1681            #Hind_rhs #Hind_lhs
1682            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
1683            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1684            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
1685            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1686            lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp)
1687            -Hvalue_eq_lhs -Hvalue_eq_rhs
1688            * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption
1689            lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm -Hsem_cmp
1690            *
1691            [ 2,4,6,8,10,12:
1692              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1693            | *: *
1694              [ 2,4,6,8,10,12:
1695                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1696              | *: *
1697                [ 2,4,6,8,10,12:
1698                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1699                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
1700            ] ] ]
1701            whd in match (eval_expr ???????);
1702            whd in match (eval_expr ???????);
1703            whd in Hsem_cmp:(??%?);
1704            destruct (Hsem_cmp)                       
1705            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1706            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1707            whd in match (m_bind ?????);
1708            whd in match (eval_binop ???????);
1709            [ 1,2,3,4,5,6:
1710              (* qed modulo integer width glitch *)
1711              @cthulhu
1712            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
1713                 lapply Heq_block_outcome -Heq_block_outcome
1714                 @(eq_block_elim … (pblock p1) (pblock p2))
1715                 normalize nodelta
1716                 [ 1,3,5,7,9,11:
1717                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
1718                   whd in match (eval_unop ????);
1719                   whd in match (m_bind ?????);
1720                   cases (cmp_offset ???) normalize nodelta
1721                   (* glitch *)
1722                   @cthulhu
1723                 | *:
1724                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1725                   whd in match (eval_unop ????);
1726                   whd in match (m_bind ?????);
1727                   @cthulhu
1728                 ]
1729           ]
1730       ]
1731    ]
1732
1733| 1: (* Integer constant *)
1734  #csz #ty cases ty
1735  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1736  | #structname #fieldspec | #unionname #fieldspec | #id ]
1737  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
1738  #val #trace #Hpresent #Hexec_cl
1739  whd in Htranslate:(??%?);
1740  [ 1,3,4,5,6,7,8: destruct ]
1741  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))))
1742  [ 2: * #H_err #H_neq_sz
1743       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1744       >Htranslate #Habsurd destruct (Habsurd) ]
1745  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1746  destruct (Heq_sz)
1747  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
1748  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
1749  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
1750| 2: *
1751  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
1752  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1753  try /2 by I/
1754  #ty whd in ⊢ (% → ?); #Hind
1755  whd in match (Plvalue ???);
1756  whd in match (typeof ?);
1757  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
1758  whd in Hexec:(??%?);
1759  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
1760  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
1761  whd in Hcl_success:(???%);
1762  [ 1: (* var case *)
1763       lapply Hcl_success -Hcl_success -Hind
1764       (* Peform case analysis on presence of variable in local Clight env.
1765        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
1766       @(match lookup SymbolTag block cl_env var_id
1767         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
1768         with
1769         [ None ⇒ λHcl_lookup. ?
1770         | Some loc ⇒ λHcl_lookup. ?
1771         ] (refl ? (lookup SymbolTag block cl_env var_id)))
1772       normalize nodelta
1773       [ 1: (* global case *)
1774            #Hlookup_global
1775            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
1776            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
1777            #Heq whd in Heq:(???%); destruct (Heq)
1778            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1779            * #var_id_alloctype * #var_id_type * #Heq
1780            cases (variable_not_in_env_but_in_vartypes_is_global …
1781                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
1782            #r #Heq' destruct (Heq') normalize nodelta
1783            lapply Hcl_load_success -Hcl_load_success
1784            lapply Hyp_present -Hyp_present
1785            lapply Hexpr_vars -Hexpr_vars
1786            lapply cm_expr -cm_expr inversion (access_mode ty)
1787            [ #typ_of_ty | | #typ_of_ty ]
1788            #Heq_typ_of_type #Heq_access_mode
1789            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1790            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1791            whd in match (eval_expr ???????);
1792            whd in match (eval_expr ???????);
1793            whd in match (eval_constant ????);
1794            <(eq_sym … inv) >Hfind_symbol normalize nodelta
1795            cases (bind_inversion ????? Hcl_load_success) #x *
1796            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
1797            lapply (opt_to_res_inversion ???? Hopt_to_res)
1798            #Hcl_load_success
1799            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1800                 @conj try @refl
1801                 whd in Hcm_load_success:(??%?);
1802                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
1803                 >(load_value_of_type_by_ref … Hcl_load_success)
1804                 try assumption %4
1805                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1806                 >Hfind_symbol normalize nodelta #Heq_embedding
1807                 whd in match (shift_offset ???);
1808                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
1809                 normalize nodelta @refl
1810            | 1: cut (access_mode ty=By_value (typ_of_type ty))
1811                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
1812                   lapply Heq_access_mode <Heqt // ] #Haccess
1813                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
1814                 #Hvalid_ptr
1815                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
1816                 [ whd in ⊢ (??%?);
1817                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1818                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
1819                 * #val' * #Hcm_load_success #Hvalue_eq
1820                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
1821                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
1822                 normalize %{val'} @conj try @refl assumption ]
1823       | 2: (* local case *)
1824            #Heq destruct (Heq)
1825            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1826            * #var_id_alloc_type * #var_id_type *
1827            generalize in match var_id_alloc_type; * normalize nodelta
1828            [ 1: #r #Hlookup_vartype
1829                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
1830                 * #typ whd in match (local_id ???);
1831                 >Hlookup_vartype normalize nodelta @False_ind
1832            | 2: (* Stack local *)
1833                 lapply Hcl_load_success -Hcl_load_success
1834                 lapply Hyp_present -Hyp_present
1835                 lapply Hexpr_vars -Hexpr_vars
1836                 lapply cm_expr -cm_expr inversion (access_mode ty)
1837                 [ #typ_of_ty | | #typ_of_ty ]
1838                 #Heq_typ_of_type #Heq_access_mode
1839                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
1840                 #stack_depth #Hlookup_vartype_success normalize nodelta
1841                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1842                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1843                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
1844                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1845                 >Hlookup' normalize nodelta #Hembedding_eq
1846                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1847                 #loaded_val * #Hload_val
1848                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1849                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1850                 #Hload_success whd in match (eval_expr ???????);
1851                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
1852                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
1853                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
1854                        >offset_plus_0 @refl ]
1855                 #Hpointer_translation
1856                 [ 2: (* By-ref *)
1857                      whd in Hload_success:(??%?);
1858                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
1859                      #Heq_val
1860                      >Heq_val
1861                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
1862                      @conj try @refl
1863                      %4 whd in match (shift_offset ???);
1864                      whd in match zero_offset;
1865                      >commutative_addition_n >addition_n_0 @Hpointer_translation
1866                 | 1: (* By value *)
1867                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
1868                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
1869                      [ @(load_by_value_success_valid_pointer … Hload_success)
1870                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
1871                      * #cm_val * #Hload_in_cm #Hvalue_eq
1872                      %{cm_val} @conj try assumption
1873                      lapply (load_value_of_type_by_value … Hload_in_cm)
1874                      [ lapply Heq_access_mode <Heq0 #Heq1
1875                        @(jmeq_to_eq ??? Heq1) ]
1876                      #Hloadv <Heq0
1877                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
1878                      >Hloadv @refl ]
1879            | 3: (* Register local variable *)
1880                 #Hlookup_eq
1881                 lapply (res_inversion ?????? Hlookup_eq)
1882                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1883                 #Htype_eq
1884                 cases (type_should_eq_inversion
1885                            var_id_type
1886                            ty
1887                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
1888                            … Htype_eq) -Htype_eq
1889                 (* Reverting all premises in order to perform type rewrite *)
1890                 #Htype_eq
1891                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
1892                 lapply Hcl_load_success -Hcl_load_success
1893                 lapply Hcl_lookup -Hcl_lookup
1894                 lapply Hyp_present -Hyp_present
1895                 lapply Hexpr_vars -Hexpr_vars
1896                 lapply cm_expr
1897                 destruct (Htype_eq)
1898                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
1899                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
1900                 destruct (Hexpr_eq)
1901                 whd in match (eval_expr ???????);
1902                 whd in match (lookup_present ?????);
1903                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1904                 >Hlookup' normalize nodelta #Hmatching
1905                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1906                 #loaded_val * #Hload_val
1907                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1908                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1909                 #Hload_success
1910                 cases (Hmatching … Hload_success) #val'
1911                 * #Hlookup_in_cm #Hvalue_eq %{val'}
1912                 cases Hyp_present
1913                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
1914                 (* seems ok *)
1915            ]
1916       ]
1917  | 2: lapply Hcl_success -Hcl_success
1918       lapply Htranslate_expr -Htranslate_expr
1919       lapply Hind -Hind cases ty1
1920       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1921       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1922       #Hind #Htranslate_expr #Hexec_cl
1923       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1924       * whd in match (typ_of_type ?); normalize nodelta
1925       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
1926       whd in ⊢ ((???%) → ?);
1927       [ 1,2,6,7: #Heq destruct (Heq) ]
1928       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
1929       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
1930       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
1931       [ 1,3,5,7: @cthulhu ]
1932       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
1933       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
1934       #Hexec_cl_ind #Hcl_ptr
1935       cut (∃ptr. cl_ptr = Vptr ptr)
1936       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
1937                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
1938       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
1939       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
1940       #Hind lapply (Hind (refl ??)) -Hind
1941       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
1942       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
1943       destruct (Hcm_ptr) #Hpointer_translation
1944       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
1945       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
1946       -Hopt_to_res
1947       lapply Hyp_present -Hyp_present
1948       lapply Hexpr_vars -Hexpr_vars
1949       lapply cm_expr -cm_expr
1950       inversion (access_mode ty)
1951       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
1952       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
1953       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1954       #Heq destruct (Heq)
1955       [ 1,2,3,4: (* By_value *)
1956           (* project Hcl_load_success in Cminor through memory_inj *)
1957           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
1958           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
1959           * #cm_val * #Hcm_load_success #Hvalue_eq
1960           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
1961           #Hloadv_cm
1962           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
1963           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
1964      | *: (* By reference *)
1965           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1966           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
1967           #Hval >Hval %4 assumption ]
1968  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
1969       lapply (refl ? (typeof e1))
1970       cases (typeof e1) in ⊢ ((???%) → %);
1971       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1972       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
1973       #Heq_typeof normalize nodelta
1974       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
1975       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
1976       normalize nodelta #Htranslate_expr
1977       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1978       * whd in match (typ_of_type ?); normalize nodelta
1979       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
1980       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
1981         #cm_field_off * #Hcm_field_off
1982       | lapply Htranslate_expr2 -Htranslate_expr2 ]
1983       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1984       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
1985       whd in Hexec_lvalue:(???%);
1986       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1987         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
1988       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1989       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1990       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
1991       [  (* Struct case *)
1992         lapply Hcl_load_value -Hcl_load_value
1993         lapply Hyp_present -Hyp_present
1994         lapply Hexpr_vars -Hexpr_vars
1995         lapply cm_expr -cm_expr
1996         lapply Hind -Hind
1997         cases ty
1998         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1999         | #structname #fieldspec | #unionname #fieldspec | #id ]
2000         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2001         normalize nodelta
2002         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2003         whd in match (eval_expr ???????);
2004         (* applying the arguments of the induction hypothesis progressively *)
2005         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
2006                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
2007         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
2008         lapply (Hind ?)
2009         [ 1,3,5,7,9:
2010            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2011            >Htranslate_expr_ind whd in match (m_bind ?????);
2012            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
2013         whd in Hoffset_eq:(???%); destruct (offset_eq)
2014         cut (cl_field_off = cm_field_off)
2015         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
2016           normalize #Heq destruct (Heq) @refl ]
2017         #Heq destruct (Heq)
2018         lapply (Hind cl_b cl_o trace ?)
2019         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
2020         lapply (Hind ?) -Hind
2021         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2022           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
2023           @Hoffset_eq ]
2024         * #cm_val' * #Heval_expr #Hvalue_eq
2025         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
2026         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
2027         [ 1,2,5: (* by-value *)
2028            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
2029            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2030            * #cm_val * #Hcm_load_value #Hvalue_eq
2031            lapply (load_value_of_type_by_value … Hcm_load_value)
2032            [ 1,3,5: @refl ]
2033            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
2034            try @refl try assumption
2035         | 3,4: (* by-ref *)
2036            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
2037            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
2038            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
2039         ]
2040      | (* union case *)
2041         lapply Hcl_load_value -Hcl_load_value
2042         lapply Hyp_present -Hyp_present
2043         lapply Hexpr_vars -Hexpr_vars
2044         lapply cm_expr -cm_expr
2045         lapply Hind -Hind
2046         cases ty
2047         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2048         | #structname #fieldspec | #unionname #fieldspec | #id ]
2049         whd in match (typ_of_type ?); normalize nodelta
2050         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2051         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2052         [ 1,2,5: (* by-value *)
2053            whd in match (eval_expr ???????);
2054            lapply (Hind cm_expr_ind Hexpr_vars ?)
2055            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
2056            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2057            -Hind #Hind
2058            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
2059            whd in match (m_bind ?????); #Hind
2060            cases (Hind (refl ??)) -Hind
2061            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
2062            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
2063            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
2064            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
2065            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2066            * #cm_val * #Hcm_load_value #Hvalue_eq           
2067            lapply (load_value_of_type_by_value … Hcm_load_value)
2068            [ 1,3,5: @refl ]
2069            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
2070            try @refl assumption
2071         | 3,4:
2072            whd in Hexec_cl:(???%); destruct (Hexec_cl)
2073            lapply (Hind cm_expr Hexpr_vars)
2074            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
2075            lapply (Hind Htranslate_expr_ind) -Hind
2076            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2077            >Hexec_lvalue whd in match (m_bind ?????);
2078            #Hind cases (Hind … Hyp_present (refl ??))
2079            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
2080            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
2081            assumption ]
2082    ]
2083  ]
2084| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
2085     whd in Hexec_lvalue_var:(??%?);
2086     (* check whether var is local or global *)
2087     lapply (Hlocal_matching var)
2088     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
2089     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
2090     normalize nodelta
2091     [ 1: (* global *)
2092          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
2093          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
2094          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
2095          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
2096          #Hembed
2097          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2098          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
2099          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
2100          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2101          whd in match (eval_expr ???????);
2102          whd in match (eval_constant ????);
2103          <(eq_sym inv var) >Hfind_symbol normalize nodelta
2104          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
2105          @conj try @refl %4 whd in match (pointer_translation ??);
2106          >Hembed normalize nodelta whd in match (shift_offset ???);
2107          >addition_n_0 @refl
2108     | 2: (* local *)
2109          #BL #Heq destruct (Heq) #_
2110          @(match (lookup ?? vars var)
2111            return λx. (lookup ?? vars var = x) → ?
2112            with
2113            [ None ⇒ ?
2114            | Some kind ⇒ ?
2115            ] (refl ??))
2116          normalize nodelta
2117          #Hlookup [ @False_ind ]
2118          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
2119          #Hlookup
2120          lapply (refl ? var_alloctype)
2121          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
2122          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
2123          [ (* stack alloc*)
2124            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2125            * #var_alloctype' #var_type' * #Hlookup_vartype'           
2126            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2127            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2128            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
2129            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
2130            @conj try @refl %4 whd in match (pointer_translation ??);
2131            >Hembed @refl
2132          | (* local alloc *)
2133            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2134            * #var_alloctype' #var_type' * #Hlookup_vartype'
2135            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2136            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2137            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
2138(*| 4: #e #ty*)
2139| 4:
2140  * #ed #ety cases ety
2141  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2142  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
2143  whd in match (typeof ?);
2144  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
2145  cases (bind_inversion ????? Htranslate) -Htranslate   
2146  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2147  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2148  * #cl_val #trace0 * #Hexec_expr #Hcl_val
2149  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
2150  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2151  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
2152  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
2153    [ 1,5,9,13: #Heq destruct (Heq)
2154    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
2155    | 3,7,11,15: #Heq destruct (Heq)
2156    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
2157  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
2158  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
2159  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
2160  %{cm_val} @conj try @refl try assumption
2161| 5:
2162  #ty cases ty
2163  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2164  | #structname #fieldspec | #unionname #fieldspec | #id ]
2165  #ed #ty' #Hind
2166  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
2167  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2168  cases (bind_inversion ????? Htranslate) -Htranslate
2169  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2170  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2171  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
2172  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2173  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2174  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
2175  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
2176  %{cm_val} @conj try @refl assumption
2177| 6:
2178  #ty *
2179  [ cases ty
2180    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2181    | #structname #fieldspec | #unionname #fieldspec | #id ]
2182    #e #Hind
2183    whd in match (typeof ?);
2184    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
2185    #Htranslate
2186    [ 3,4,5,8: destruct (Htranslate)
2187    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2188         cases sz normalize nodelta
2189         #e' #Hexpr_vars #Htranslate
2190         [ 1, 2: destruct (Htranslate) ] ]
2191    #cl_val #trace #Hyp_present #Hexec_expr
2192    cases (bind_inversion ????? Htranslate) -Htranslate
2193    #cmop * #Htranslate_unop #Hexec_arg
2194    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2195    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2196    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2197    * #cl_arg #cl_trace * #Hexec_cl
2198    whd in ⊢ ((???%) → ?); #Hexec_unop
2199    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2200    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2201    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2202    #Hsem_cl whd in match (eval_expr ???????);
2203    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2204    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2205    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
2206    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
2207    whd in match (typ_of_type Tvoid);
2208    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
2209    #H >H @refl
2210  | *:
2211    cases ty
2212    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
2213    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
2214    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
2215    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
2216    whd in Htranslate:(??%?);
2217    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
2218    cases (bind_inversion ????? Htranslate) -Htranslate
2219    #cmop * #Htranslate_unop #Hexec_arg
2220    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2221    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2222    cases (bind_inversion ????? Hexec) -Hexec
2223    * #cl_arg #cl_trace * #Hexec_cl
2224    whd in ⊢ ((???%) → ?); #Hexec_unop
2225    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2226    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2227    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2228    #Hcl_unop whd in match (eval_expr ???????);
2229    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2230    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2231    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
2232    * #op_res * #Hcl_sem #Hvalue_eq
2233    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
2234       %{op_res} @conj try @refl assumption
2235    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
2236       %{op_res} @conj try @refl assumption
2237    ]
2238  ]
2239| 8: #ty #ty' * #ed #ety
2240  cases ety
2241  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2242  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2243  whd in match (typeof ?); whd in match (typ_of_type ?);
2244  #Hind whd in match (typeof ?);
2245  #cm_expr #Hexpr_vars #Htranslate
2246  cases (bind_inversion ????? Htranslate) -Htranslate
2247  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
2248  cases (bind_inversion ????? Htranslate) -Htranslate
2249  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
2250  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
2251  cases (bind_inversion ????? Htranslate) -Htranslate
2252  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
2253  #Heq destruct (Heq)
2254  #cl_val #trace #Hyp_present #Hexec_cm
2255  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2256  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
2257  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
2258  #cast_val * #Hexec_cast
2259  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2260  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
2261  #Htype_eq
2262  lapply Hexec_cast -Hexec_cast
2263(*  lapply Htyp_should_eq -Htyp_should_eq *)
2264  lapply Htranslate_cast -Htranslate_cast
2265  lapply Hexpr_vars_cast -Hexpr_vars_cast
2266  lapply cm_cast -cm_cast
2267  lapply Hyp_present -Hyp_present
2268  lapply Hexpr_vars -Hexpr_vars
2269  lapply cm_expr -cm_expr
2270  <Htype_eq -Htype_eq
2271  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
2272  whd in match (typeof ?); normalize nodelta
2273  cases ty'
2274  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2275  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2276  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2277  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
2278  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2279  whd in Htranslate_cast:(??%%);
2280  whd in Hexpr_vars;
2281  destruct (Htranslate_cast)
2282  [ 1,2,3,4,7:
2283    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2284    * #cm_val' * #Heval_castee
2285    lapply Hexec_cm -Hexec_cm
2286    whd in Hexec_cast:(??%%);
2287    cases cm_val in Hexec_cast; normalize nodelta
2288    [ | #vsz #vi | | #vp
2289    | | #vsz #vi | | #vp
2290    | | #vsz #vi | | #vp
2291    | | #vsz #vi | | #vp
2292    | | #vsz #vi | | #vp ]
2293    [ 2,6,10,14,18:
2294    | *: #Habsurd destruct (Habsurd) ]
2295    #Hexec_cast #Hexec_cm #Hvalue_eq
2296    [ 1,2,3:
2297      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
2298      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
2299    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
2300    [ 1,2,4,5:
2301      cases (bind_inversion ????? Hexec_cast)
2302      whd in match (typeof ?);
2303      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
2304      whd in match (eq_rect_r ??????);
2305      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
2306      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
2307      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
2308      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
2309      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2310      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
2311      >Heval_castee normalize nodelta whd in match (eval_unop ????);
2312      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
2313      >Heq_vi >eq_bv_true normalize
2314      %{Vnull} @conj try @refl %3
2315    | 3: destruct (Hcl_val_eq)
2316          whd in match (eval_expr ???????);
2317          >Heval_castee normalize nodelta
2318          whd in match (eval_unop ????);
2319          cases esg normalize nodelta
2320          whd in match (opt_to_res ???); whd in match (m_bind ?????);
2321          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
2322          whd in match (eq_rect_r ??????);
2323          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
2324          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
2325             this reason. *)
2326          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
2327          cases esz normalize nodelta
2328          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
2329          whd in match (sign_ext ??); whd in match (zero_ext ??);
2330          %2
2331    ]
2332 | *:
2333    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2334    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
2335    %{cm_val'} @conj try @refl
2336    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
2337    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
2338    cases cm_val
2339    [ | #vsz #vi | | #vp
2340    | | #vsz #vi | | #vp
2341    | | #vsz #vi | | #vp
2342    | | #vsz #vi | | #vp ]
2343    #Hexec_cm #Hvalue_eq #Hexec_cast
2344    whd in Hexec_cast:(??%%);
2345    [ 1,5,9,13: destruct (Hexec_cast) ]
2346    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
2347    lapply Hexec_cast -Hexec_cast
2348    normalize cases (eq_v ?????) normalize
2349    #Habsurd destruct (Habsurd)
2350 ]
2351| 9: (* Econdition *) 
2352  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
2353  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
2354  #Hexec_cm
2355  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2356  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
2357  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2358  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
2359  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2360  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
2361  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2362  cases (bind_inversion ????? Htranslate) -Htranslate
2363  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2364  cases (bind_inversion ????? Htranslate) -Htranslate
2365  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2366  cases (bind_inversion ????? Htranslate) -Htranslate
2367  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
2368  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
2369  *  #Htypeof_e2_eq_ty
2370  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2371  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
2372  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
2373  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2374  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
2375  cases (bind_inversion ????? Htranslate) -Htranslate
2376  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
2377  cases (bind_inversion ????? Htranslate) -Htranslate 
2378  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
2379  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
2380  * #Htypeof_e3_eq_ty
2381  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
2382  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
2383  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
2384  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2385  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
2386  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
2387  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
2388  lapply Hexec_bool_of_val -Hexec_bool_of_val
2389  cases (typeof e1) normalize nodelta
2390  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2391  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2392  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
2393  whd in Heq:(???%); destruct (Heq)
2394  whd in match (eval_expr ???????);
2395  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
2396  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
2397  >Heval_e1 normalize nodelta
2398  lapply Hcm_ifthenelse -Hcm_ifthenelse
2399  lapply Hexec_cond -Hexec_cond 
2400  lapply Hexec_bool_of_val -Hexec_bool_of_val
2401  lapply Hvalue_eq1 -Hvalue_eq1
2402  cases cm_cond_val
2403  [ | #vsz #vi | | #vp
2404  | | #vsz #vi | | #vp
2405  | | #vsz #vi | | #vp
2406  | | #vsz #vi | | #vp ]
2407  whd in ⊢ (? → (??%%) → ?);
2408  [ 6:
2409  | *: #_ #Habsurd destruct (Habsurd) ]
2410  #Hvalue_eq1 #Hsz_check
2411  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2412  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2413  #Heq destruct (Heq)
2414  #Hexec_expr_e1
2415  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
2416    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
2417    with
2418    [ true ⇒ λHeq. ?
2419    | false ⇒ λHeq. ?
2420    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
2421  normalize nodelta
2422  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
2423  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
2424  >Heq normalize nodelta
2425  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
2426    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
2427    normalize %{cm_val3} @conj try @refl assumption
2428  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
2429    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
2430    normalize %{cm_val2} @conj try @refl assumption ]
2431| 10: (* andbool *)
2432  #ty cases ty
2433  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2434  | #structname #fieldspec | #unionname #fieldspec | #id ]
2435  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2436  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2437  (* decompose first slice of clight execution *)
2438  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2439  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2440  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2441  #b * #Hexec_bool_of_val #Hexec_expr
2442  (* decompose translation to Cminor *)
2443  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2444  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2445  cases (bind_inversion ????? Htranslate) -Htranslate
2446  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
2447  [ 2: | *: #Heq destruct (Heq) ]
2448  (* discriminate I16 and I8 cases *)
2449(*  lapply Hyp_present -Hyp_present
2450  lapply Hexpr_vars -Hexpr_vars
2451  lapply cm_expr -cm_expr cases sz
2452  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
2453  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
2454  (* go on with decomposition *)
2455  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
2456  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
2457  (* cleanup the type coercion *)
2458  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
2459  * #Htypeof_e2_eq_ty
2460  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2461  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
2462  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2463  lapply Hexpr_vars_e2 -Hexpr_vars_e2
2464  lapply cm_expr_e2 -cm_expr_e2
2465  lapply Hexec_expr -Hexec_expr
2466  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
2467  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2468  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
2469  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
2470   * to proceed in decomposing translation. *)
2471  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2472  lapply Hexpr_vars_e1 -Hexpr_vars_e1
2473  lapply cm_expr_e1 -cm_expr_e1
2474  lapply Hexec_bool_of_val -Hexec_bool_of_val
2475  cases (typeof e1)
2476  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2477  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
2478  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
2479  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2480  (* translation decomposition terminated. Reduce goal *)
2481  whd in match (eval_expr ???????);
2482  (* We need Hind1.  *)
2483  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
2484  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
2485  normalize nodelta
2486  (* peform case analysis to further reduce the goal. *)
2487  lapply Hvalue_eq -Hvalue_eq
2488  lapply Hexec_bool_of_val -Hexec_bool_of_val
2489  whd in match (proj2 ???);
2490  cases cl_val_e1
2491  [ | #vsz #vi | | #vp
2492  | | #vsz #vi | | #vp
2493  | | #vsz #vi | | #vp
2494  | | #vsz #vi | | #vp ]
2495  whd in ⊢ ((??%%) → ?);
2496  [ 6:
2497  | *: #Heq destruct (Heq) ]
2498  #Hsz_check #Hvalue_eq
2499  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2500  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2501  (* preparing case analysis on b *)
2502  lapply Hexec_expr -Hexec_expr
2503  cases b normalize nodelta
2504  [ 2: (* early exit *)
2505       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
2506       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
2507       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
2508       <e0 whd in match (m_bind ?????);
2509       @cthulhu
2510       (* Pb: incompatible semantics for cl and cm.
2511        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
2512          first operand is false (for andbool)
2513          . solution 1 : change semantics to return actual value instead of Vfalse
2514          . solution 2 : change toCminor to introduce another test in the program,
2515            returning Vfalse in case of failure instead of actual value
2516        *) ]
2517  #Hexec_expr #Heq_outcome
2518  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2519  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
2520  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2521  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
2522  #Heq destruct (Heq)
2523  >(value_eq_int_inversion … Hvalue_eq)
2524  whd in match (eval_bool_of_val ?);
2525  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
2526  normalize nodelta
2527  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
2528  >Heval_expr normalize nodelta
2529  %{cm_val_e2} @conj try @refl 
2530  whd in Hexec_bool_outcome:(??%%);
2531  normalize nodelta in Hexec_bool_outcome:(??%%);
2532  lapply Hvalue_eq2 -Hvalue_eq2
2533  -Heval_expr
2534  lapply Hexec_bool_outcome -Hexec_bool_outcome
2535  cases cl_val_e2
2536  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
2537  #Heq destruct (Heq)
2538  cases (intsize_eq_elim_inversion ??????? Heq)
2539  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2540  cases outcome_bool normalize nodelta
2541  (* Problem. cf prev case. *)
2542  @cthulhu
2543| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
2544| 12: (* sizeof *)
2545  #ty cases ty
2546  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2547  | #structname #fieldspec | #unionname #fieldspec | #id ]
2548  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2549  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
2550  normalize in match (typ_of_type ?);
2551  whd in Htranslate:(??%?); destruct (Htranslate)
2552  whd in match (eval_expr ???????);
2553  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
2554| 13:
2555  #ty #ed #ty' cases ty'
2556  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2557  | #structname #fieldspec | #unionname #fieldspec | #id ]
2558  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2559  #Hexec_lvalue
2560  whd in Hexec_lvalue:(??%?); destruct
2561  [ whd in Htranslate_addr:(??%?);
2562    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2563    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
2564    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2565    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
2566    #Heq destruct (Heq)
2567    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
2568  ]
2569  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2570  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
2571  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
2572       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
2573       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
2574       #cm_val_field * #Heval_cm #Hvalue_eq
2575       whd in match (eval_expr ???????);
2576       >Heval_cm normalize nodelta
2577       whd in match (eval_expr ???????); whd in match (m_bind ?????);
2578       whd in match (eval_binop ???????); normalize nodelta
2579       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
2580       normalize nodelta #Hptr_translate
2581       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
2582       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
2583       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
2584       cases (E cl_blo) in Hptr_translate; normalize nodelta
2585       [ #H destruct (H) ]
2586       * #BL #OFF normalize nodelta #Heq destruct (Heq)
2587       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
2588       #H destruct (H)
2589       (* again, mismatch in the size of the integers *)
2590       @cthulhu
2591  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
2592       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
2593       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
2594       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
2595       #Hpointer_translation
2596       %{cm_val} @conj try assumption
2597       destruct @refl
2598   ]
2599| 14: (* cost label *)
2600  #ty (* cases ty
2601  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2602  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
2603  #l * #ed #ety
2604  whd in match (typeof ?); whd in match (typeof ?);
2605  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2606  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2607  #Hexpr_vars * #Htranslate_ind #Htranslate
2608  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2609  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2610  whd in match (typeof ?) in Htyp_should_eq:(??%?);
2611  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
2612  #Htyp_eq
2613  lapply Htranslate_ind -Htranslate_ind
2614  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2615  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2616  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2617  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
2618  <Htyp_eq
2619  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
2620  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2621  whd in match (eval_expr ???????);
2622  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2623  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2624  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2625  #cm_val' * #Heval_expr' #Hvalue_eq
2626  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
2627  >cons_to_append >(nil_append … cm_trace) @refl
2628| 15: *
2629  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
2630  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
2631  #ty normalize in ⊢ (% → ?);
2632  [ 2,3,12: @False_ind
2633  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2634           normalize #Habsurd destruct (Habsurd) ]
2635] qed.
2636
2637
2638axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
2639
2640(* Conjectured simulation results
2641
2642   We split these based on the start state:
2643   
2644   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
2645      normal steps in Cminor;
2646   2. call and return steps are simulated by a call/return step plus [m] normal
2647      steps (to copy stack allocated parameters / results); and
2648   3. lone cost label steps are simulates by a lone cost label step
2649   
2650   These should allow us to maintain enough structure to identify the Cminor
2651   subtrace corresponding to a measurable Clight subtrace.
2652 *)
2653
2654definition clight_normal : Clight_state → bool ≝
2655λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2656
2657definition cminor_normal : Cminor_state → bool ≝
2658λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2659
2660axiom clight_cminor_normal :
2661  ∀INV:clight_cminor_inv.
2662  ∀s1,s1',s2,tr.
2663  clight_cminor_rel INV s1 s1' →
2664  clight_normal s1 →
2665  ¬ Clight_labelled s1 →
2666  ∃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〉) →
2667  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2668    tr = tr' ∧
2669    clight_cminor_rel INV s2 s2'
2670  ).
2671
2672axiom clight_cminor_call_return :
2673  ∀INV:clight_cminor_inv.
2674  ∀s1,s1',s2,tr.
2675  clight_cminor_rel INV s1 s1' →
2676  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2677  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2678  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2679    tr = tr' ∧
2680    clight_cminor_rel INV s2 s2'
2681  ).
2682
2683axiom clight_cminor_cost :
2684  ∀INV:clight_cminor_inv.
2685  ∀s1,s1',s2,tr.
2686  clight_cminor_rel INV s1 s1' →
2687  Clight_labelled s1 →
2688  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2689  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2690    tr = tr' ∧
2691    clight_cminor_rel INV s2 s2'
2692  ).
2693
Note: See TracBrowser for help on using the repository browser.